This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Timing Analysis of Ada Tasking Programs
July 1996 (vol. 22 no. 7)
pp. 461-483

Abstract—Concurrent real-time software is increasingly used in safety-critical embedded systems. Assuring the quality of such software requires the rigor of formal methods. In order to analyze a program formally, we must first construct a mathematical model of its behavior. In this paper, we consider the problem of constructing such models for concurrent real-time software. In particular, we provide a method for building mathematical models of real-time Ada tasking programs that are accurate enough to verify interesting timing properties, and yet abstract enough to yield a tractable analysis on nontrivial programs. Our approach differs from schedulability analysis in that we do not assume that the software has a highly restricted structure (e.g., a set of periodic tasks). Also, unlike most abstract models of real-time systems, we account for essential properties of real implementations, such as resource constraints and run-time overhead.

[1] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[2] R. Alur and D. Dill, "Automata for Modeling Real-Time Systems," Proc. 17th Int'l Colloq. Aut. Lang. Prog., 1990.
[3] R. Alur and R. Kurshan, "Timing Verification by Successive Approximation," Information and Computation, vol. 118, no. 1, pp. 142-157, Apr. 1995.
[4] E. Ashcroft and Z. Manna, "Formalization of Properties of Parallel Programs," Machine Intelligence, vol. 6, pp. 17-41, 1971.
[5] G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden, "Automated Analysis of Concurrent Systems with the Constrained Expression Toolset," IEEE Trans. Software Eng. vol. 17, no. 11, pp. 1204-1222, Nov. 1991.
[6] G.S. Avrunin, J.C. Corbett, L.K. Dillon, and J.C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IEEE Trans. Software Eng., vol. 20, no. 9, 1994.
[7] J.G.P. Barnes, Programming in Ada.Reading, Mass.: Addison-Wesley, 1995.
[8] B. Berthomieu and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Trans. Software Eng., vol. 17, no. 3, Mar. 1991.
[9] J.C. Corbett, "Modeling and Analysis of Real-Time Ada Tasking Programs," K. Ramamritham, ed., Proc. Real-Time Systems Symp., IEEE CS Press, pp. 132-141, Dec. 1994.
[10] J.C. Corbett, "A Method for Timing Analysis of Ada Tasking Programs," Technical Report ICS-TR-95-17, Information and Computer Science Department, Univ. of Hawaii at Ma noa, Dec. 1995.
[11] J.C. Corbett, "Constructing Abstract Models of Concurrent Real-Time Software," S. Ziel, ed., Proc. 1996 Int'l Symp. Software Testing and Analysis (ISSTA). ACM Press, Jan. 1996.
[12] J.C. Corbett, “Evaluating Deadlock Detection Methods for Concurrent Software,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161–179, Mar. 1996.
[13] J.C. Corbett and G.S. Avrunin, "A Practical Method for Bounding the Time Between Events in Concurrent Real-Time Systems," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker [37], New York: ACM Press, pp. 110-116, June 1993.
[14] P. Cousot and N. Halbwachs, “Automatic Discovery of Linear Restraints among Variables of a Program,” Proc. Fifth Ann. ACM Symp. Principles of Programming Languages, pp. 84–97, Jan. 1978.
[15] A.N. Fredette and R. Cleaveland, "RTSL: A Formal Language for Real-Time Schedulability Analysis," Proc. Real-Time Systems Symp., pp. 274-283, 1993.
[16] R. Gerber and I. Lee, "A Layered Approach to Automating the Verification of Real-Time Systems," IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768-784, Sept. 1992.
[17] 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.
[18] C. Ghezzi, D. Mandriolli, and A. Morzenti, "Trio: A Logic Language for Executable Specifications of Real-Time Systems," J. Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
[19] E.W. Giering and T.P. Baker, "Using POSIX Threads to Implement Ada Tasking: Description of Work in Progress," Proc. TriAda '92, pp. 518-529, 1992.
[20] E.W. Giering and T.P. Baker, "The Gnu Ada Runtime Library (GNARL): Design and Implementation," Proc. 11th Ann. Washington Ada Symp. Summer ACM SIG Ada Meeting (WAdaS '94), June 1994.
[21] M. Srinivas and L.M Patnaik,"Learning neural network weights using genetic algorithms—Improving performance by search space reduction," Proc. 1991 IEEE Int'l Joint Conf. Neural Networks,Singapore, pp. 18-21, 1991.
[22] M.G. Harbour, M.H. Klein, and J.P. Lehoczky, “Timing Analysis for Fixed Priority Scheduling of Hard Real Time Systems,” IEEE Trans. Software Eng., vol. 20, no. 1, pp. 13-28, Jan. 1994.
[23] T. Henzinger and P.-H. Ho, "HyTech: The Cornell Hybrid Technology Tool," Proc. 1994 Workshop on Hybrid Systems and Autonomous Control, Lecture Notes in Computer Science. New York: Springer-Verlag, 1995.
[24] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: The Next Generation," Proc. Real-Time Systems Symp., IEEE CS Press, 1995.
[25] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "A User Guide to HyTech," Technical Report CSD-TR-95-1532, Department of Computer Science, Cornell Univ., 1995.
[26] 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.
[27] S. Lim et al., "An Accurate Worst Case Timing Analysis Technique for RISC Processors," Proc. 15th IEEE Real-Time Systems Symp., pp. 97-108,San Juan, Puerto Rico, Dec. 1994.
[28] 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.
[29] X. Nicollin, J. Sifakis, and S. Yovine, “Compiling Real-Time Specifications into Extended Automata,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 794-804, Sept. 1992.
[30] J.S. Ostroff, “Deciding properties of Timed Transition Models,” IEEE Trans. Paralel and Distributed Systems, vol. 1, no. 2, Apr. 1990.
[31] C.Y. Park and A.C. Shaw, "Experiments With a Program Timing Tool Based on Source-Level Timing Schema," Computer, pp. 48-57, May 1991.
[32] K. Ramamritham ed., Proc. Real-Time Systems Symp. IEEE CS Press, Dec. 1994.
[33] G.M. Reed and A.W. Roscoe, "A Timed Model for Communicating Sequential Processes," Theoretical Computer Science, vol. 58, pp. 249-261, June 1988.
[34] A.C. Shaw, "Reasoning About Time in Higher-Level Language Software," IEEE Trans. Software Eng., vol. 15, no. 7, pp. 875-889, 1989.
[35] R.N. Taylor, "A General-Purpose Algorithm for Analyzing Concurrent Programs," Comm. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[36] U.S. Department of Defense, Reference Manual for the Ada Programming Language, ANSI/MIL-STD-1815A. Washington, D.C.: Government Printing Office, Jan. 1983.
[37] W. Zhao, K. Ramamritham, and J.A. Stankovic, “Scheduling Tasks with Resource Requirements in Hard Real Time Systems,” IEEE Trans. Software Eng., vol. 13, no. 5, pp. 564-577, May 1987.

Index Terms:
Timing analysis, real-time systems, program verification, hybrid systems, Ada tasking.
Citation:
James C. Corbett, "Timing Analysis of Ada Tasking Programs," IEEE Transactions on Software Engineering, vol. 22, no. 7, pp. 461-483, July 1996, doi:10.1109/32.538604
Usage of this product signifies your acceptance of the Terms of Use.