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

Issue

9

fYear

1986

Firstpage

890

Lastpage

904

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;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/TSE.1986.6313045

Filename

6313045