SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Mechanized Verification of Real-Time Systems Using PVS
 by Dr. Natarajan Shankar.

Some important properties of certain safety-critical systems can only be established by a careful analysis of their real-time behavior. These systems are typically also designed to meet other functional requirements where the real-time behavior is irrelevant. A suitable verification framework for such systems must therefore be capable of coping with functional as well as real time behavior. 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 introducing a new operator for reasoning about absolute time. This operator returns the amount of time that has elapsed since the given predicate last held in the current computation. This approach is mechanized by first encoding the computational behavior of real-time systems within the higher-order logic of PVS and employing the interactive proof checker of PVS to develop the proofs. Our approach is illustrated using two examples: Fischer's real-time mutual exclusion protocol and a railroad crossing controller. \Ve also discuss related approaches to formalizing real-time behavior.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy