Fair Synchronous Transition Systems and Their Liveness Proofs

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 sts model KP96] 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 speci cations, and provide a sound and compositional proof system for it. This research was supported in part by the Minerva Foundation, by an infrastructure grant from the Israeli Ministry of Science, by US National Science Foundation grants CCR9509931 and CCR-9712383, and by US Air Force O ce of Scienti c Research Contract No. F4...

• Type: Conference
• Year: 1998
• Where: FTRTFT
• Authors: Amir Pnueli, Natarajan Shankar, Eli Singerman
• Keywords: Basic Sts Model, Fair Synchronous Transitions, Formal Methods, FTRTFT 1998, Synchronous Speci Cations