Constructing abstract models of concurrent real-time software

ABSTRACT

Concurrent real-time software is used in many safety-critical applications. Assuring the quality of such software requires the use of formal methods. Before a program can be analyzed formally, however, we must construct a mathematical model that captures the aspects of the program we want to verify. In this paper, we show how to construct mathematical models of concurrent real-time software that are suitable for analyzing the program's timing properties. 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 more abstract models of real-time systems, we account for essential properties of real implementations, such as resource constraints and run-time overhead.

REFERENCES

• 1: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 2: Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
• 3: Bernard Berthomieu , Michel Diaz, Modeling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE Transactions on Software Engineering, v.17 n.3, p.259-273, March 1991 [doi>10.1109/32.75415]
• 4: J. C. Corbett. Modeling and analysis of real-time Ada tasking programs, in Ramamritham {15}, pages 132-141.
• 5: A. N. Fredette and R. Cleaveland. RTSL: a formal language for real-time schedulability analysis. In Proceedings of the Real-Time Systems Symposium, pages 274-283, 1993.
• 6: Richard Gerber , Insup Lee, Guest A Layered Approach to Automating the Verification of Real-Time Systems, IEEE Transactions on Software Engineering, v.18 n.9, p.768-784, September 1992 [doi>10.1109/32.159838]
• 7: Carlo Ghezzi , Dino Mandrioli , Sandro Morasca , Mauro Pezzè, A Unified High-Level Petri Net Formalism for Time-Critical Systems, IEEE Transactions on Software Engineering, v.17 n.2, p.160-172, February 1991 [doi>10.1109/32.67597]
• 8: C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
• 9: E. W. Giering, III , T. P. Baker, The GNU Ada runtime library (GNARL), Proceedings of the eleventh annual Washington Ada symposium & summer ACM SIGAda meeting on Ada, p.97-107, July 1994, McLean, Virginia, United States [doi>10.1145/197978.197989]
• 10: M. G. Harbour , M. H. Klein , J. P. Lehoczky, Timing Analysis for Fixed-Priority Scheduling of Hard Real-Time Systems, IEEE Transactions on Software Engineering, v.20 n.1, p.13-28, January 1994 [doi>10.1109/32.263752]
• 11: F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
• 12: S.Lim, Y. Bae, G.T. Jang, B.Rhee, S. Min, C.Y. Park, H. Shin, K. Park, and C. S. Kim. An accurate worst case timing analysis technique for RISC processors. In Ramamritham {15}, pages 97-108.
• 13: J. S. Ostroff, Deciding Properties of Timed Transition Models, IEEE Transactions on Parallel and Distributed Systems, v.1 n.2, p.170-183, April 1990 [doi>10.1109/71.80145]
• 14: Chang Yun Park , Alan C. Shaw, Experiments with a Program Timing Tool Based on Source-Level Timing Schema, Computer, v.24 n.5, p.48-57, May 1991 [doi>10.1109/2.76286]
• 15: K. Ramamritham, editor. Proceedings of the Real- Time Systems Symposium. IEEE Computer Society Press, Dec. 1994.
• 16: G. M. Reed , A. W. Roscoe, A timed model for communicating sequential processes, Theoretical Computer Science, v.58 n.1-3, p.249-261, June 1988 [doi>10.1016/0304-3975(88)90030-8]
• 17: A. C. Shaw, Reasoning About Time in Higher-Level Language Software, IEEE Transactions on Software Engineering, v.15 n.7, p.875-889, July 1989 [doi>10.1109/32.29487]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.9 Management
          Subjects: Time estimation

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

General Terms:
Design, Theory