We present an approach to the verification of the real-time behavior of concurrent programs and describe its mechanization using the PVS proof checker. Our approach to real-time behavior extends previous verification techniques for concurrent programs by proposing a simple model for real-time computation and introducing a new operator for reasoning about absolute time. This model is formalized and mechanized within the higher-order logic of PVS. The interactive proof checker of PVS is used to develop the proofs of two illustrative examples: Fischer’s real-time mutual exclusion protocol and a railroad crossing controller.
CITATION STYLE
Shankar, N. (1993). Verification of real-time systems using PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 280–291). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_23
Mendeley helps you to discover research relevant for your work.