Safety analysis of timing properties in real-time systems
Generate an AI Snapshot to get a quick, structured summary of this paper.
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The authors formalize the safety analysis of timing properties in real-time systems based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems.
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.