This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Safety analysis of timing properties in real-time systems
Sept. 1986 (vol. 12 no. 9)
pp. 890-904
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.
Index Terms:
Real-time systems,Timing,Safety,Clocks,Syntactics,Computational modeling,Time factors,verification,Real time,real-time logic,safety analysis,systems specification,time-critical system
Citation:
Farnam Jahanian, Aloysius Ka-Lau Mok, "Safety analysis of timing properties in real-time systems," IEEE Transactions on Software Engineering, vol. 12, no. 9, pp. 890-904, Sept. 1986, doi:10.1109/TSE.1986.6313045
Usage of this product signifies your acceptance of the Terms of Use.