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.

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.

@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/}
}

• cav93-realtime.dvi
• cav93-realtime.pdf
• cav93-realtime.ps