Issue No. 07 - July (1996 vol. 22)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.538604
<p><b>Abstract</b>—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.</p>
Timing analysis, real-time systems, program verification, hybrid systems, Ada tasking.
J. C. Corbett, "Timing Analysis of Ada Tasking Programs," in IEEE Transactions on Software Engineering, vol. 22, no. , pp. 461-483, 1996.