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

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

Lecture Notes in Computer Science, Volume 697.
From Computer Aided Verification, CAV '93.
Edited by Costas Courcoubetis.
Springer-Verlag, Elounda, Greece.
June/July, 1993.
Pages 280–291.


Abstract
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. We also discuss related approaches to formalizing real-time behavior.
BibTEX Entry
@inproceedings{cav93-realtime,
    AUTHOR = {{N.} Shankar},
    TITLE = {Verification of Real-Time Systems Using {PVS}},
    BOOKTITLE = {Computer Aided Verification, {CAV} '93},
    YEAR = {1993},
    EDITOR = {Costas Courcoubetis},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {697},
    PAGES = {280--291},
    ADDRESS = {Elounda, Greece},
    MONTH = {June/July},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cav93-realtime/}
}
Files
 













 

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