Issue No. 09 - Sept. (1986 vol. 12)
Farnam Jahanian , Department of Computer Sciences, University of Texas at Austin, Austin, TX 78712
Aloysius Ka-Lau Mok , Department of Computer Sciences, University of Texas at Austin, Austin, TX 78712
Two important characteristics of time-critical systems are: the requirement to satisfy stringent timing constraints, and the need to guard against an imperfect execution environment. In this paper, we formalize the safety analysis of timing properties in real-time systems. Our analysis is based on a formal logic: RTL (Real-Time Logic) which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, our goal is to relate the safety assertion to the systems specification. There are three distinct cases: 1) the safety assertion is a theorem derivable from the systems specification, 2) ine safety assertion is unsatisfiable with respect to the systems specification, or 3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis will be presented.
Real-time systems, Timing, Safety, Clocks, Syntactics, Computational modeling, Time factors, verification, Real time, real-time logic, safety analysis, systems specification, time-critical system
F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems," in IEEE Transactions on Software Engineering, vol. 12, no. , pp. 890-904, 1986.