This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
On Inspection and Verification of Software with Timing Requirements
August 2003 (vol. 29 no. 8)
pp. 705-720

Abstract—Software with hard timing requirements should be designed using a systematic approach to make its timing properties easier to inspect and verify; otherwise, it may be practically impossible to determine whether the software satisfies the timing requirements. Preruntime scheduling provides such an approach by placing restrictions on software structures to reduce complexity. A major benefit of using a preruntime scheduling approach is that it makes it easier to systematically inspect and verify the timing properties of the actual software code, not just various high-level abstractions of the code.

[1] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems Hybrid Systems, R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, eds., 1993.
[2] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[3] R. Alur and T.A. Henzinger, Real-Time Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390-401, 1990.
[4] R. Alur and T. Henzinger, "Logics and Models of Real-Time: A Survey," Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, pp. 74-106.
[5] S.R. Ball, Debugging Embedded Microprocessor Systems. Newnes, 1998.
[6] S.R. Ball, Embedded Microprocessor Systems: Real World Design, second ed. Newnes, 2000.
[7] P. Bellini, R. Mattolini, and P. Nesi, Temporal Logics for Real-Time System Specification ACM Computing Surveys, vol. 32, no. 1, pp. 12-42, 2000.
[8] A. Burns, K. Tindell, and A. Wellings, “Effective Analysis for Engineering Real-Time Fixed Priority Schedulers,” IEEE Trans. Software Eng., vol. 21, no. 5, pp. 475-480, May 1995.
[9] S.V. Campos and E.M. Clarke, The Verus Language: Representing Time Efficiently with BDDs Theoretical Computer Science, 1999.
[10] G.D. Carlow, Architecture of the Space Shuttle Primary Avionics Software System Comm. ACM, vol. 27, pp. 926-936, Sept. 1984.
[11] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[12] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Progress on the State Explosion Problem in Model Checking Informatics. 10 Years Back. 10 Years Ahead, R. Wilhelm, ed., 2001.
[13] E.M. Clarke and J.M. Wing, "Formal Methods: State of the Art and Future Directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, 1996.
[14] E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venter, D. Weil, and S. Yovine, TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems Proc. 13th Int'l Conf. Computer Aided Verification (CAV), pp. 391-395, 2001.
[15] D. Cofer and M. Rangarajan, Formal Modeling and Analysis of Advanced Scheduling Features in an Avionics RTOS Proc. Int'l Workshop Embedded Software (EMSOFT 2002), A. Sangiovanni-Vincentelli and J. Sifikis, eds., 2002.
[16] P. Chou and G. Borriello, "Modal Processes: Towards Enhanced Retargetability Through Control Composition of Distributed Embedded Systems," Proc. Design Automation Conf., June 1998.
[17] P. Cousot and R. Cousot, Verification of Embedded Software: Problems and Perspectives Proc. Int'l Workshop Embedded Software (EMSOFT 2001), 2001.
[18] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Hybrid Systems III, R. Alur, T.A. Henzinger, and E.D. Sontag, eds., 1996.
[19] E.W. Dijkstra, Cooperating Sequential Processes Programming Languages, F. Genuys, ed., pp. 43-112, 1968.
[20] D. Dill and J. Rushby, Acceptance of Formal Methods: Lessons from Hardware Design Computer, vol. 29, pp. 23-24, 1996.
[21] B. Dutertre, Formal Analysis of the Priority Ceiling Protocol Proc. IEEE Real-Time Systems Symp., pp. 151-160, Nov. 2000.
[22] E.A. Emerson and E.M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons Science of Computer Programming, vol. 2, pp. 241-266, 1982.
[23] E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan, Quantitative Temporal Reasoning Proc. Second Workshop Computer-Aided Verification, pp. 136-145, 1989.
[24] S.R. Faulk and D.L. Parnas, On Synchronization in Hard-Real-Time Systems Comm. ACM, vol. 31, pp. 274-287, Mar. 1988.
[25] J.G. Ganssle, The Art of Designing Embedded Systems. Newnes, 2000.
[26] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezze, “A Unified High-Level Petri Net Formalism for Time-Critical Systems,” IEEE Trans. Software Eng., vol. 17, no. 2, pp. 160–171, Feb. 1991.
[27] C. Heitmeyer, "On the Need for Practical Formal Methods," Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98),Lyngby, Denmark, Sept. 1998.
[28] K. Heninger, J. Kallander, D.L. Parnas, and J. Shore, Software Requirements for the A-7E Aircraft NRL Report No. 3876, Nov. 1978.
[29] T.A. Henzinger, Z. Manna, and A. Pnueli, "Temporal Proof Methodologies for Real-Time Systems," Proc. 18th Ann. ACM Symp. Principles of Programming Languages, pp. 353-366, 1990.
[30] T.A. Henzinger and J.-F. Raskin, Robust Undecidability of Timed and Hybrid Systems Proc. Third Int'l Workshop Hybrid Systems: Computation and Control, 2000.
[31] Software Fundamentals: Collected Papers by David L. Parnas. D.M. Hoffman and D.M. Weiss, eds., Addison-Wesley, 2001.
[32] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[33] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[34] M. H. Klein, T. Ralya, B. Pollak, R. Obenza, and M. G. Harobur,A Practitioner's Handbook for Real-Time Analysis: Guide to Rate Monotonic Analysis for Real-Time Systems. New York: Kluwer–Academic, 1993.
[35] H. Kopetz, Real-Time Systems Design Principles for Distributed Embedded Applications, Kluwer Academic, Boston, 1997.
[36] C.L. Liu and J.W. Layland, “Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environment,” J. ACM, vol. 20, no. 1, pp. 40-61, 1973.
[37] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[38] M.P. Melliar-Smith and R. L. Schwartz, Formal Specification and Mechanical Verification of SIFT: A Fault-Tolerant Flight Control System IEEE Trans. Computers, vol. 31, no. 7, pp. 616-629, July 1982.
[39] A.K. Mok, Fundamental Design Problems of Distributed Systems for the Hard-Real-Time Environment PhD thesis, Dept. of Electrical Eng. and Computer Science, Massachusetts Inst. of Technology, Cambridge, Mass., May 1983.
[40] A.K. Mok, The Design of Real-Time Programming Systems Based on Process Models Proc. IEEE Real-Time Systems Symp., pp. 5-17, Dec. 1984.
[41] J. Ostroff, Temporal Logic for Real-Time Systems. John Wiley and Sons, 1989.
[42] D.L. Parnas, Inspection of Safety-Critical Software Using Program-Function Tables Proc. IFIP World Congress 1994, vol. 3, Aug. 1994.
[43] J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger, Verification of Time Partitioning in the DEOS Scheduler Kernel Proc. Int'l Conf. Software Eng., pp. 488-497, 2000.
[44] J.-P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337-351, Lecture Notes in Computer Science 137, Springer-Verlag, Apr. 1982.
[45] L. Sha, R. Rajkuma, and J.P. Lehoczky, "Priority Inheritance Protocols: An Approach to Real-Time Synchronization," IEEE Trans. Computers, vol. 39, no. 9, pp. 1,175-1,185, Sept. 1990.
[46] T. Shepard and M. Gagne, A Model of the F-18 Mission Computer Software for Preruntime Scheduling Proc. 10th Int'l Conf. Distributed Computing Systems, pp. 62-69, 1990.
[47] T. Shepard and M. Gagne, “A Pre-Run-Time Scheduling Algorithm for Hard Real-Time Systems,” IEEE Trans. Software Eng., vol. 17, no. 7, pp. 669-677, July 1991.
[48] W. Soukoreff, A Comparison of Two Preruntime Schedule-Dispatchers for RTAI COSC6390 Project Report, Dept. of Computer Science, York Univ., Dec. 2001.
[49] Hard Real-Time Systems IEEE Computer Society Tutorial, J. Stankovic and K. Ramamrithan, eds., 1988.
[50] J.A. Stankovic, M. Spuri, M. Di Natale, and G. Buttazzo, “Implications of Classical Scheduling Results for Real-Time Systems,” IEEE Computer, vol. 28, no. 6, June 1995.
[51] J. Xu, “Multiprocessor Scheduling of Processes with Release Times, Deadlines, Precedence, and Exclusion Relations,” IEEE Trans. Software Eng., vol. 19, no. 2, pp. 139-154, Feb. 1993.
[52] J. Xu, Making Timing Properties of Software Easier to Inspect and Verify IEEE Software, July/Aug. 2003.
[53] J. Xu and K.-y. Lam, Integrating Runtime Scheduling and Preruntime Scheduling of Real-Time Processes Proc. 23rd IFAC/IFIP Workshop Real-Time Programming, June 1998.
[54] J. Xu and D.L. Parnas, “Scheduling Processes with Release Times, Deadlines, Precedence and Exclusion Relations,” IEEE Trans. Software Eng., vol. 16, no. 3, pp. 360-369, Mar. 1990.
[55] J. Xu and D.L. Parnas, Preruntime Scheduling of Processes with Exclusion Relations on Nested or Overlapping Critical Sections Proc. 11th Ann. IEEE Int'l Phoenix Conf. Computers and Comm. (IPCCC-92), Apr. 1992.
[56] J. Xu and D.L. Parnas, "On Satisfying Timing Constraints in Hard Real-Time Systems," IEEE Trans. Software Eng., Vol. 19, No. 1, Jan. 1993, pp. 70-84.
[57] J. Xu and D.L. Parnas, Fixed Priority Scheduling versus Pre-Run-Time Scheduling Real-Time Systems, vol. 18, pp. 7-23, Jan. 2000.

Index Terms:
Real-time, software, code, inspection, verification, timing requirements, current practices, complexity, restrictions, software structures, preruntime scheduling, predictability.
Citation:
Jia Xu, "On Inspection and Verification of Software with Timing Requirements," IEEE Transactions on Software Engineering, vol. 29, no. 8, pp. 705-720, Aug. 2003, doi:10.1109/TSE.2003.1223645
Usage of this product signifies your acceptance of the Terms of Use.