Title :
Safety analysis of timing properties in real-time systems
Author :
Jahanian, Farnam ; Mok, Aloysius Ka-lau
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
Abstract :
The authors formalize the safety analysis of timing properties in real-time systems. The 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, the 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) the 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 is presented.
Keywords :
formal logic; real-time systems; safety; systems analysis; RTL; formal logic; formal specification; real-time logic; real-time systems; safety analysis; safety assertion; systems specification; timing properties; Clocks; Computational modeling; Real-time systems; Safety; Syntactics; Time factors; Timing; Real time; real-time logic; safety analysis; systems specification; time-critical system; verification;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1986.6313045
