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

Fair Synchronous Transition Systems and their Liveness Proofs
 by Dr. Natarajan Shankar, Amir Pnueli & Eli Singerman.

Lecture Notes in Computer Science, Volume 1486.
From 5th International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '98).
Springer Verlag, Lyngby, Denmark.
September, 1998.
Pages 198–209.


Abstract
We present a compositional semantics of synchronous systems that captures both safety and progress properties of such systems. The fair synchronous transitions systems (FSTS) model we introduce in this paper extends the basic ASTS model of Kesten and Pnueli by introducing operations for parallel composition, for the restriction of variables, and by addressing fairness. We introduce a weak fairness (justice) condition which ensures that any communication deadlock in a system can only occur through the need for external synchronization. We present an extended version of linear time temporal logic (ELTL) for expressing and proving safety and liveness properties of synchronous specifications, and provide a sound and compositional proof system for it.
BibTEX Entry
@inproceedings{Pnueli&Shankar&Singerman98,
    AUTHOR = {Amir Pnueli and Natarajan Shankar and Eli Singerman},
    TITLE = {Fair Synchronous Transition Systems and their Liveness Proofs},
    BOOKTITLE = {5th International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '98)},
    YEAR = {1998},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {1486},
    PAGES = {198--209},
    ADDRESS = {Lyngby, Denmark},
    MONTH = {sep},
    PUBLISHER = {Springer Verlag},
    URL = {http://www.csl.sri.com/papers/csl-98-2/}
}
Files
 













 

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