
Verification of RealTime Systems Using PVS
by Dr. Natarajan Shankar.
Lecture Notes in Computer Science, Volume 697. From Computer Aided Verification, CAV '93. Edited by Costas Courcoubetis. SpringerVerlag, Elounda, Greece. June/July, 1993. Pages 280–291.
Abstract
We present an approach to the verification of the realtime behavior of concurrent programs
and describe its mechanization using the PVS proof checker. Our approach to realtime
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 realtime systems
within the higherorder logic of PVS and employing the interactive proof checker of PVS to
develop the proofs. Our approach is illustrated using two examples: Fischer's realtime
mutual exclusion protocol and a railroad crossing controller. We also discuss related
approaches to formalizing realtime behavior.
BibT_{E}X Entry
@inproceedings{cav93realtime,
AUTHOR = {{N.} Shankar},
TITLE = {Verification of RealTime Systems Using {PVS}},
BOOKTITLE = {Computer Aided Verification, {CAV} '93},
YEAR = {1993},
EDITOR = {Costas Courcoubetis},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {697},
PAGES = {280291},
ADDRESS = {Elounda, Greece},
MONTH = {June/July},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/cav93realtime/}
}
Files

