This Article 
 Bibliographic References 
 Add to: 
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.
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.