Fair Synchronous Transition Systems and their Liveness Proofs ^{∗}

Amir Pnueli Dept. of Applied Math. and CS The Weizmann Institute of Science Rehovot, ISRAEL

Natarajan Shankar Eli Singerman Computer Science Laboratory SRI International Menlo Park CA, USA

Technical Report SRI-CSL-98-02

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 α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 specifications, 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 CCR-9509931 and CCR-9712383, and by US Air Force Office of Scientific Research Contract No.

F49620-95-C0044. Part of this research was done as part of the European Community project SACRES (EP 20897). The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NSF, AFOSR, the European Union, or the U.S. Government.

We are grateful to Sam Owre for lending assistance with PVS.

1 Introduction

Synchronous languages are rapidly gaining popularity as a high-level programming paradigm for a variety of safety-critical and real-time control applications and for hardware/software co-design. Synchronous languages are used to define systems that are:

• Reactive: Engaged in an ongoing interaction with an environment.

• Event-triggered: System computation is triggered by the arrival and absence of external inputs.

• Concurrent: A system is composed of subsystems that are computing and interacting concurrently.

• Synchronous: The system response to input stimuli is “instantaneous”.

The present paper presents a unifying transition system model for synchronous languages based on fair synchronous transition systems (fsts) that can be used as a semantic basis for synchronous languages. Such a unifying semantic model can be used to specify the temporal behavior of synchronous systems and to relate different synchronous system descriptions.

There are two major classes of synchronous languages [H93]. The imperative languages like Esterel [BG92] and Statecharts [Har87], and declarative languages like Lustre [CHPP87] and Signal [BGJ91]. The language Esterel has statements like:

• present signal then statement else statement: Execute then statement when signal is present, and else statement otherwise.

• emit signal : broadcast signal.

• trap id in … exit id …: A catch-throw mechanism for exception signaling and handling.

• do statement watching signal: preempt execution of statement when signal occurs.

These are combined with the usual control constructs like conditional branching and parallel composition.

Declarative languages like Lustre and Signal express constraints on signal flows or infinite streams. In Lustre, each signal is defined in a mutually recursive way in terms of other signals. Lustre applies the various logical and arithmetic operators in a pointwise manner to signals so that X + Y is the signal that is the pointwise sum of signals X and Y. The basic operators for constructing expressions that define signals in Lustre are:

• pre(X) which is nil, x_{0}, x_{1}, …, where X is x_{0}, x_{1}, . . ..

• X -> Y which is the signal x_{0}, y_{1}, y_{2}, … where X is of the form x_{0}, x_{1}, …, and Y is of the form y_{0}, y_{1}, . . ..

• X when B which is the signal ⟨x_{i} | b_{i}⟩, i.e., the sequences x_{i_{1}}, x_{i_{2}}, …,, where i_{1}, i_{2}, …, are the positions at which the boolean signal B is true. The resulting clock of X when B is defined by the boolean signal B.

• current X which speeds up X to the next faster clock in terms of which X is defined. This is done by padding X with the previous x_{i} wherever X is undefined with respect to the faster clock.

For example,

B  t  f  t  f  f  t  t  f  f …
X  1  2  3  4  5  6  7  8  9 …
X when B  1  3  6  7  …
current (X when B)  1  1  3  3  3  6  7  8  8 …

Lustre programs are functional with respect to the input streams. All Lustre signals in a program are defined with respect to sub-clocks of a single master clock.

The language Signal is the most liberal of the synchronous languages and is the primary motivation for the fair synchronous transition systems model presented here. Signal is similar to Lustre but admits the specification of nondeterministic constraints and the signals are not all derived from a single master clock.

Signal programs may also contain mutually recursive definitions of signals. Apart from the usual pointwise arithmetic, logical, and other data operators, the basic operators in Signal are:

• X $ init y_{0} which is the signal having the same clock as X and the same signal as X but delayed by one clock tick and with initial value y_{0}.

• X when B is similar to the corresponding operator in Lustre but X and B can have different clocks. The clock of the resulting signal is the intersection of the two clocks and takes on the value of X whenever the boolean signal B is true.

• X default Y is the signal whose clock is the union of the clocks of X and Y and whose value is equal to the value of X when X is defined, and the value of Y otherwise.

Signal programs can be combined by parallel composition P∥Q which is the conjunction of the equations in P and Q. Hiding P/X is another operation where an externally visible signal X in P can be made local to a program P/X.

The features common to all these synchronous languages are that • Signals are not persistent and can be present or absent in a computation

state.

• State transitions can be governed by the presence of a signal in a state, its value when it is present, and its absence.

• A module specifies constraints on the signal values in each transition.

• Composition yields the conjunction of such constraints since in synchronous systems, the synchronized transitions occur simultaneously.

In this paper, we present a compositional semantics of synchronous systems that captures both safety and progress properties of such systems. The semantics is given in terms of the model of fair synchronous transitions systems (fsts), which is based on the αsts model [KP96]. The αsts model has been used as a common semantic domain for both Signal programs and the C-code generated by compiling them, for proving the correctness of the translation (compilation) [PSS98]. It has also been used in [BGA97] as a semantics which is “...fully general to capture the essence of the synchronous paradigm.”

The fsts model presented here extends αsts by introducing operations for parallel composition, for the restriction of variables, and by addressing fairness. It can be used to answer questions such as:

• What is the valid set of runs corresponding to a given synchronous specification?

• How can we characterize a set of fair computations corresponding to a given synchronous specification?

• How can linear time temporal logic be adapted to reasoning about fair synchronous specifications?

• What is a sound compositional proof system for proving temporal safety and liveness properties of synchronous specifications?

The key characteristics of the fsts model that make it suitable for capturing the semantics of synchronous systems are:

• Signals are modeled by variables whose value might be undefined in a state indicating the absence of the signal.

• The absence of a signal is indicated by having the values of variables range over a lifted domain that contains an undefined ⊥ value in addition to defined data values.

• The variables of a transition system module are partitioned into

– Synchronization variables that are used for interaction through input and output with other modules.

– Controlled variables which are entirely controlled by the system consisting of variables that are externally visible and those that are local.

• Transitions can be taken on the basis of whether a signal is present or absent in a state.

• The crucial compositionality constraints on a fsts module are :

– A module transition cannot force the synchronization variables to take on defined values. It should always be possible for the system to enter a communication deadlock where the synchronization variables all remain undefined. This is because the module and its environment need to cooperate in order to synchronize on a defined value for a synchronization variable, and it is always possible for the environment to not cooperate with the module.

– A module transition is invariant with respect to the part of the state that is unobservable by it. The behavior of the module is only affected by another module through the values (defined or undefined) of the synchronization variables that they share.

– If any signal that is controlled by the module is continuously disabled, i.e., undefined, it must be because its definedness depends on the definedness of some subset of synchronization variables. This restriction is captured by means of a justice (weak fairness) condition that ensures that a variable that is continuously enabled to take on a defined value even when the synchronization variables are deadlocked, does eventually do so. The justice condition requires controlled variables to not deadlock, i.e., remain undefined, unless their definedness depends on the values of synchronization variables.

The fsts model is designed to be simple and general. It extends the classical notion of transition systems with signals that can be present or absent in a given state, communication as synchronization by means of signals, stuttering as the absence of signals, and local progress through weak fairness constraints. The fairness condition ensures that any communication deadlock in a module can only occur through the need for external synchronization. Except for the fairness condition, the presence or absence of a signal is treated in a symmetrical manner as is the case in synchronous languages. The use of weak fairness constraints ensures that a module can satisfy these constraints without the cooperation of the environment, i.e., the module is receptive [AL95].

The fsts model, the compositionality proofs, the extended linear temporal logic, and the accompanying soundness proofs have all been formally verified using PVS [Ow95]. The PVS verification pointed out a number of gaps in our earlier formalization and led to sharper definitions of the basic concepts, and elegant and rigorous proofs.^{1}

The paper is organized as follows. In Section 2 we introduce the fsts computational model. In Section 3 we define two important operations on fsts modules, parallel composition and restriction, and motivate the definitions by an intuitive example of progress (liveness). In Section 4 we present a formal method for proving temporal properties of synchronous systems by introducing an appropriate logic for expressing these properties and a system of deductive proof rules. We demonstrate the use of these rules by formalizing the intuitive arguments used in the example of Section 3. In Section 5 we present the fsts semantics of the most expressive synchronous language – Signal. (The fsts semantics of Esterel and Lustre can be obtained in a similar way.)

2 Fair Synchronous Transition Systems

In this section, we introduce the notion of fair synchronous transition systems.

The Computational Model

We assume a vocabulary V which is a set of typed variables. Variables which are intended to represent signals are identified as volatile, and their domain contains a distinguished element ⊥ used to denote the absence of the respective signal. In the translation of synchronous programs to fsts specifications (see Section 5), we shall also use persistent variables to simulate the “memorization” operators of the synchronous languages (e.g., current in Lustre, “$” in Signal).

Some of the types we consider are the booleans with domain B = {t, f}, the type of integers whose domain Z consists of all the integers, the type of pure signals with domain S_{⊥} = {t, ⊥}, the type of extended booleans with domain B_{⊥} = {t, f, ⊥}, and the type of extended integers with domain Z_{⊥} = Z ∪ {⊥}.

We define a state s to be a type-consistent interpretation of V, assigning to each variable u ∈ V a value s[u] over its domain. We denote by Σ the set of all states. For a subset of variables V ⊆ V, we define a V -state to be a type-consistent interpretation of V.

Following [MP91] and [KP96], we define a fair synchronous transition system (fsts) to be a system

Φ: ⟨V, Θ, ρ, E, S⟩,

consisting of the following components:

• V : A finite set of typed system variables.

• Θ : The initial condition. A satisfiable assertion characterizing the initial states.

1The PVS formalization and proofs can be obtained from the URL www.csl.sri.com/~singermn/fsts/.

• ρ : A transition relation. This is an assertion ρ(V, V′), which relates a state s ∈ Σ to its possible successors s′ ∈ Σ by referring to both unprimed and primed versions of the system variables. An unprimed version of a system variable refers to its value in s, while a primed version of the same variable refers to its value in s′. For example, the assertion x′ = x + 1 states that the value of x in s′ is greater by 1 than its value in s. If ρ(s[V], s′[V]) = t, we say that state s′ is a ρ-successor of state s.

Remark: As implied by the notation ρ(V, V′), ρ can only refer to the variables of Φ, and therefore cannot distinguish between two possible Φsuccessors that agree on the values of all the variables of Φ. That is, for all s, s_{1}, s_{2} ∈ Σ,

s_{1}|V = s_{2}|V → (ρ(s, s_{1}) ⇔ ρ(s, s_{2})) .

• E ⊆ V : The set of externally observable variables. These are the variables that can be observed outside the module. We refer to L = V − E as the local variables. Local variables cannot be observed outside the module.

• S ⊆ E : The set of synchronization variables. These are the signal variables on which the module may (and needs to) synchronize with its environment. We refer to C = V − S as the controllable variables. These are the variables on whose values the module has full control.

For states s, s′ ∈ Σ and assertion φ(V, V′), we say that φ holds over the joint interpretation ⟨s, s′⟩, denoted

⟨s, s′⟩ ⊧ φ,

if φ(V, V′) evaluates to t over the interpretation which interprets every x ∈ V as s[x] and every x′ as s′[x].

For an fsts Φ, a state s′ is called a Φ-successor of the state s if ⟨s, s′⟩ ⊧ ρ.

Definition 1 An fsts Φ is called realizable if every state s ∈ Σ has a Φsuccessor in which all the synchronization variables assume the value ⊥. This requirement expresses the possibility that the environment might not be ready to co-operate with the module Φ in the current state.

From now on, we restrict our attention to realizable fsts specifications.

Computations of an FSTS

Let Φ = ⟨V, Θ, ρ, E, S⟩ be an fsts. A computation of Φ is an infinite sequence

σ: s_{0}, s_{1}, s_{2}, …,

where, for each i = 0, 1, …, s_{i} ∈ Σ, and σ satisfies the following requirements:

• Initiation: s_{0} is initial, i.e., s_{0} ⊧ Θ.

• Consecution: For each j = 0, 1, …, s_{j+1} is a Φ-successor of s_{j}.

• Justice (weak fairness): We say that a signal variable x ∈ C is enabled with respect to S at state s_{j} of σ if there exists a Φ-successor s of s_{j}, such that s[x] ≠ ⊥ ∧ s[S] = {⊥}.

The justice requirement is that for every signal variable x ∈ C, it is not the case that x is enabled w.r.t. S in all but a finite number of states along σ, while s_{j}[x] ≠ ⊥, for only finitely many states s_{j} in the computation.

Remark: In the sequel, we shall sometimes use the term “enabled w.r.t. Φ” instead of “enabled w.r.t. S_{Φ}”.

The requirement of justice with respect to a controllable signal variable x demands that if x is continuously enabled to assume a non-⊥ value, from a certain point on, without the need to synchronize with the environment, it will eventually assume such a value. The fact that a variable x is enabled to become non-⊥ without ‘external assistance’ is evident from the existence of a Φ-successor s such that s[x] ≠ ⊥ ∧ s[S] = {⊥}.

A run of a system Φ is a finite or an infinite sequence of states satisfying the requirements of initiation and consecution, but not necessarily the requirement of justice.

An fsts is called viable if every finite run can be extended into a computation. From now on, we restrict our attention to viable fsts specifications.

For the case that Φ is a finite-state system, i.e., all system variables range over finite domains, there exist (reasonably) efficient symbolic model-checking algorithms for testing whether Φ is viable.

A state s′ is a stuttering variant of a state s if all volatile (i.e., signal) variables are undefined in s′ and s′ agrees with s on all persistent variables. A state sequence σ̂ is said to be a stuttering variant of the state sequence σ : s_{0}, s_{1}, …, if σ̂ can be obtained from σ by repeated transformations where a state s in σ is replaced with s, s′ in σ̂, or a pair of adjacent states s, s′ in σ is replaced with s in σ̂ where s′ is a stuttering variant of s. A set of state sequences S is called closed under stuttering if, for every state sequence σ, σ ∈ S iff all stuttering variants of σ belong to S. An fsts Φ is called stuttering robust if the set of Φ-computations is closed under stuttering.

3 Operations on FSTS Modules

There are two important operations on fsts modules: parallel composition and restriction.

3.1 Parallel Composition

Let Φ_{1}: ⟨V_{1}, Θ_{1}, ρ_{1}, E_{1}, S_{1}⟩ and Φ_{2}: ⟨V_{2}, Θ_{2}, ρ_{2}, E_{2}, S_{2}⟩ be two fsts modules. These systems are called syntactically compatible if they satisfy

C_{1} ∩ V_{2} = V_{1} ∩ C_{2} = ∅ (or equivalently V_{1} ∩ V_{2} = S_{1} ∩ S_{2}).

That is, only synchronization variables can be common to both systems. We define the parallel composition of syntactically compatible Φ_{1} and Φ_{2}, denoted Φ = Φ_{1} ∥ Φ_{2}, to be the fsts Φ: ⟨V, Θ, ρ, E, S⟩, where

\begin{aligned}V & = & V_{1} ∪ V_{2} \\ Θ & = & Θ_{1} ∧ Θ_{2} \\ ρ & = & ρ_{1} ∧ ρ_{2} \\ E & = & E_{1} ∪ E_{2} \\ S & = & S_{1} ∪ S_{2} \end{aligned}

To indicate the relation between computations of a composed system and computations of its constituents, we first prove the following lemma:

Lemma 1 Let Φ_{1}: ⟨V_{1}, Θ_{1}, ρ_{1}, E_{1}, S_{1}⟩ and Φ_{2}: ⟨V_{2}, Θ_{2}, ρ_{2}, E_{2}, S_{2}⟩ be two compatible fsts modules, x be a controlled signal variable of Φ_{1}, and σ: s_{0}, s_{1}, s_{2}, … be a sequence of states. For every j ≥ 0:

x is enabled in s_{j} w.r.t. Φ_{1} ⟺ x is enabled in s_{j} w.r.t. Φ_{1} ∥ Φ_{2}.

Proof: (⟹) First, note that since x is a controlled signal variable of Φ_{1}, it is also a controlled signal variable of Φ_{1} ∥ Φ_{2}. Now, assume that s is a Φ_{1}-successor of s_{j}, s.t. s[x] ≠ ⊥ and s[S_{1}] = ⊥. By the realizability requirement applied to Φ_{2} (see Definition 1), there exists a state s′, s.t. ρ_{2}(s, s′) and s′[S_{2}] = ⊥. Let s′′ be the state that valuates each variable of Φ_{1} as s and all other variables as s′. Since Φ_{1} and Φ_{2} are syntactically compatible, we have s′′[x] ≠ ⊥ and s′′[S_{1} ∪ S_{2}] = ⊥. Hence, by recalling that ρ_{1} and ρ_{2} can only refer to variables in V_{1} and V_{2}, respectively, we have that ρ_{1}(s, s′′) and ρ_{2}(s, s′′); i.e., s′′ is a Φ_{1} ∥ Φ_{2}-successor of s_{j}, and we are done.

The argument in the other direction is similar. We can now prove the following theorem:

Theorem 2 Let Φ_{1}: ⟨V_{1}, Θ_{1}, ρ_{1}, E_{1}, S_{1}⟩ and Φ_{2}: ⟨V_{2}, Θ_{2}, ρ_{2}, E_{2}, S_{2}⟩ be two compatible fsts modules, and σ: s_{0}, s_{1}, s_{2}, … be a sequence of states.

σ is a computation of Φ_{1} ∥ Φ_{2} ⟺ σ is both a computation of Φ_{1} and of Φ_{2}.

Proof: (⟹) Due to symmetry, it suffices to prove that σ is a computation of Φ_{1}. The fact that σ satisfies the initiation and consecution requirements for Φ_{1} follows easily from the definition of Φ_{1} ∥ Φ_{2}. What remains is to show that σ is fair (just) w.r.t. Φ_{1}. Let x be a controlled variable of Φ_{1} which is continuously enabled w.r.t. Φ_{1}. We have to prove that x ≠ ⊥ infinitely often. By Lemma 1, we conclude that x is continuously enabled w.r.t. Φ_{1} ∥ Φ_{2}. So, by the assumption that σ is a computation of Φ_{1} ∥ Φ_{2}, and is therefore just w.r.t. Φ_{1} ∥ Φ_{2}, we have x ≠ ⊥ infinitely often.

(⟸) Again, it is easy to see that σ satisfies the the initiation and consecution requirements for Φ_{1} ∥ Φ_{2}. To prove that σ is fair w.r.t. Φ_{1} ∥ Φ_{2}, let x be a controlled variable of Φ_{1} ∥ Φ_{2} which is continuously enabled w.r.t. Φ_{1} ∥ Φ_{2}. By the definition of Φ_{1} ∥ Φ_{2}, x ∈ (V_{1} \ S_{1}) ∪ (V_{2} \ S_{2}). Without loss of generality, assume x ∈ (V_{1} \ S_{1}), i.e., x is a controlled variable of Φ_{1}. Using Lemma 1, we see that x is continuously enabled w.r.t. Φ_{1}, so that by the fact that σ is fair w.r.t. to Φ_{1}, we have x ≠ ⊥ infinitely often.

3.2 Restriction

In the operation of restriction, we identify a set of synchronization variables and close off the system for external synchronization on these variables.

Let W ⊆ S be a set of synchronization variables of the fsts Φ: ⟨V, Θ, ρ, E, S⟩. We define the W -restriction of Φ, denoted [own W: Φ], to be the fsts Φ̃: ⟨Ṽ, Θ̃, ρ̃, Ẽ, S̃⟩, where

\begin{aligned}Ṽ & = & V \\ Θ̃ & = & Θ \\ ρ̃ & = & ρ \\ Ẽ & = & E \\ S̃ & = & S \ W. \end{aligned}

Thus the effect of W -restricting the system Φ amounts to moving the variables in W from S to C. This movement may have a considerable effect on the computations of the system.

Example 1 Consider the fsts Φ, where

\begin{aligned}V = E = S & : & \{x : \{t, ⊥\}\} \\ Θ & : & x = t \\ ρ & : & x′ = t ∨ x′ = ⊥. \end{aligned}

Let Φ̃: [own x. Φ] denote the x-restriction of Φ. The sequence below, in which next to each state appears the set of all possible successors,

σ: \begin{matrix}s_{0}: ⟨x: t⟩, & \{⟨x: ⊥⟩, ⟨x: t⟩\} \\ s_{1}: ⟨x: ⊥⟩, & \{⟨x: ⊥⟩, ⟨x: t⟩\} \\ s_{2}: ⟨x: ⊥⟩, & … \end{matrix}

is a computation of Φ but is not a computation of Φ̃. Note that x assumes a non-⊥ value only at s_{0}. The sequence σ is a computation of Φ since x is not in C (x ∈ S), and therefore is not enabled w.r.t. S in any state of σ. On the other hand, x is no longer a synchronization variable in Φ̃, since it belongs to C̃. The sequence σ is not a computation of Φ̃ since it is unfair to x. This is because now, x is enabled w.r.t. S_{Φ} in every state of σ, but s[x] ≠ ⊥ only in s_{0}. From this we can deduce that all computations of Φ̃ contain infinitely many states in which x ≠ ⊥, but this is not necessarily the case for computations of Φ.

The following lemma (whose proof is left for the final version) describes the relation between computations of unrestricted and restricted systems.

Lemma 3 The infinite sequence

σ: s_{0}, s_{1}, s_{2}, …

is a computation of [own W. Φ] iff

1. σ is a computation of Φ, and

2. σ satisfies the justice requirement w.r.t. S \ W.

Thus, the computations of [own W. Φ] can be obtained from those of Φ.

Example 2 Consider the fsts Φ_{1} defined by

\begin{aligned}V_{1} = E_{1} & : & \{x, y : Z_{⊥}\} \\ S_{1} & : & \{x\} \\ Θ_{1} & : & x = y = ⊥ \\ ρ_{1} & : & (y′ = 3) ∧ (x′ = 4) ∨ (y′ = ⊥) ∧ (x′ ≠ 4) \end{aligned}

and the fsts Φ_{2} defined by

\begin{aligned}V_{2} = E_{2} = S_{2} & : & x : Z_{⊥} \\ Θ_{2} & : & x = ⊥ \\ ρ_{2} & : & (x′ = 4) ∨ (x′ = 5) ∨ (x′ = ⊥). \end{aligned}

Both of these fsts modules have computations satisfying � � (y = 3). There exists, however, a computation of both Φ_{1} and Φ_{2} which by Theorem 2 is therefore also a computation of Φ_{1} ∥ Φ_{2}, which does not satisfy � � (y = 3). This computation is

σ: \begin{matrix}s_{0}: ⟨⊥^{x}, ⊥^{y}⟩, & \{⟨⊥, ⊥⟩, ⟨4, 3⟩, ⟨5, ⊥⟩\} \\ s_{1}: ⟨⊥, ⊥⟩, & \{⟨⊥, ⊥⟩, ⟨4, 3⟩, ⟨5, ⊥⟩\} \\ s_{2}: ⟨⊥, ⊥⟩, & … \end{matrix}

In σ, the variable y does not get the value 3 even once. This is fair, since y is not enabled w.r.t. S_{Φ_{1}∥Φ_{2}} in any state of σ. This is because y′ ≠ ⊥ ∧ x′ = ⊥ is false in every state of σ. Now, suppose we close off Φ with respect to x, to get the fsts module

Φ̃: [own x. [Φ_{1} ∥ Φ_{2}]].

In Φ̃, x is no longer a synchronization variable, and therefore y is continuously enabled w.r.t. S_{Φ} in σ (in every state, in fact). However, it is obviously not the case that y ≠ ⊥ is satisfied infinitely often in σ, and hence σ is not a computation of Φ̃. In conclusion, we see that only the restriction of x guarantees � � (y = 3).

4 Compositional Verification of fsts Modules

In this section we show how to construct compositional verification of the temporal properties of fsts’s, concentrating on liveness properties. First, we define an appropriate logic. Let eltl be ltl extended with the unary predicate ready. An eltl model is a pair M = (L, σ), where σ is an infinite sequences of the form

σ: s_{0}, s_{1}, s_{2}, …, where s_{j} ∈ Σ, for every j ≥ 0,

and L : Σ → 2^{Σ}. eltl formulas are interpreted as follows.

• For a state formula p, (M, j) ⊧ p ↔ s_{j} ⊧ p.

• (M, j) ⊧ ¬p ↔ (M, j) |̸= p.

• (M, j) ⊧ p ∨ q ↔ (M, j) ⊧ p or (M, j) ⊧ q.

• (M, j) ⊧ � p ↔ (M, j + 1) ⊧ p.

• (M, j) ⊧ p U q ↔ (M, k) ⊧ q for some k ≥ j and (M, i) ⊧ p for all i, j ≤ i < k.

• For a state formula p, (M, j) ⊧ ready(p) ↔ ∃s ∈ L(s_{j}) s.t. s ⊧ p.

As usual, we use the abbreviations � p for t U p and � p for ¬ � ¬p.

We say that a model M satisfies an eltl formula p, written M ⊧ p, if (M, 0) ⊧ p.

Notation: For an eltl model M = (L, σ), we denote by σ(i), the i + 1-th element of σ.

For an fsts Φ, the eltl model M = (L, σ) is called a Φ-model, if

1. σ is a computation of Φ, and

1. Φ_{1} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}), where {z_{1}, …, z_{n}} ⊇ S_{Φ_{1}} ∩ S_{Φ_{2}}
2. Φ_{2} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n})
Φ_{1} ∥ Φ_{2} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n})

Figure 1: Rule ready.

2. For every j = 0, 1, 2, …, L(σ(j)) is the set of all possible Φ-successors of σ(j), i.e., L(σ(j)) = image(ρ, {σ(j)}).

We write Φ ⊧ p, and say that p is valid over Φ, if M ⊧ p, for every Φ-model M.

Definition 2 An eltl formula is called universal, if it does not contain ready or if each occurrence of ready appears under an odd number of negations.

We present our method by formalizing the intuitive arguments used in Example 2. In the proof, we introduce several deductive rules that we believe may be useful in typical liveness proofs. The soundness of these rules is proved in the sequel.

Let us begin by noting that

Φ_{1}, Φ_{2} ⊧ � ready(y = 3 ∧ x = 4),  (1)

can be verified independently for Φ_{1} and for Φ_{2}. From (1) and the temporal tautology q → � q, we can derive

Φ_{1}, Φ_{2} ⊧ � � ready(y = 3 ∧ x = 4).  (2)

Applying rule ready, presented in Fig. 1, to (2) yields

Φ_{1} ∥ Φ_{2} ⊧ � � ready(y = 3 ∧ x = 4).  (3)

From the latter, we can easily derive

Φ_{1} ∥ Φ_{2} ⊧ � � ready(y ≠ ⊥).  (4)

By applying rule own (Fig. 2) to (4), with W = {x}, we get

\underbrace{[own x. [Φ_{1} ∥ Φ_{2}]]}_{Φ} ⊧ � � ready(y ≠ ⊥).  (5)

Now, since S_{Φ} = ∅, we can use axiom cont (Fig. 3), and (5) with z = y, to derive

Φ ⊧ � � (y ≠ ⊥).  (6)

Φ ⊧ p, where p ∈ eltl

[own W. Φ] ⊧ p

Figure 2: Rule own.

Φ ⊧ � � ready(z ≠ ⊥ ∧ S_{Φ} = ⊥) → � � (z ≠ ⊥), where z ∈ C_{Φ}

Figure 3: Axiom cont.

It is not difficult to prove

Φ_{1} ⊧ � (y = 3 ∨ y = ⊥).  (7)

By applying rule comp (Fig. 4) to the latter, we get

Φ_{1} ∥ Φ_{2} ⊧ � (y = 3 ∨ y = ⊥).  (8)

We now apply rule own (Fig. 2) to (8), to get

Φ ⊧ � (y = 3 ∨ y = ⊥).  (9)

The latter, together with (6) implies Φ ⊧ � � (y = 3) which completes the proof.

Now, as promised, we prove the soundness of the deductive rules. We start with two lemmas that follow from Theorem 2, and characterize the relation between eltl models of a composed system and those of its constituents.

Lemma 4 Let Φ_{1} and Φ_{2} be two compatible fsts modules, M_{1} = (L_{1}, σ) be a Φ_{1}-model, and M_{1} = (L_{2}, σ) be a Φ_{2}-model. Then

(L_{∩}, σ) is a Φ_{1} ∥ Φ_{2} -model, where L_{∩}(s) = L_{1}(s) ∩ L_{2}(s), for every s ∈ Σ.

Lemma 5 Let Φ_{1} and Φ_{2} be two compatible fsts modules, and M = (L, σ) be a Φ_{1} ∥ Φ_{2}-model. Then

(L_{Φ_{1}}, σ) is a Φ_{1} -model, where L_{Φ_{1}}(s) = image(ρ_{Φ_{1}}, {s}), for every s ∈ Σ.

Theorem 6 The rule ready is sound. That is, let Φ_{1}: ⟨V_{1}, Θ_{1}, ρ_{1}, E_{1}, S_{1}⟩ and Φ_{2}: ⟨V_{2}, Θ_{2}, ρ_{2}, E_{2}, S_{2}⟩ be two compatible fsts’s, and {z_{1}, …, z_{n}} be a set of Φ_{1} ⊧ p, where p ∈ eltl is universal

Φ_{1} ∥ Φ_{2} ⊧ p

Figure 4: Rule comp.

variables s.t. {z_{1}, …, z_{n}} ⊇ S_{1} ∩ S_{2}:

(Φ_{1} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n})) ∧
(Φ_{2} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}))) →
(Φ_{1} ∥ Φ_{2} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n})).

Proof: [(sketch)] Let M = (L, σ) be a Φ_{1} ∥ Φ_{2}-model. Use Lemma 5 to construct a Φ_{1}-model, M_{1} = (L_{Φ_{1}}, σ), and a Φ_{2}-model, M_{2} = (L_{Φ_{2}}, σ). By the assumption,

M_{1} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}) and
M_{2} ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}).

Hence, there exists an i_{0} s.t. for all j ≥ i_{0},

(M_{1}, j) ⊧ ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}) and
(M_{2}, j) ⊧ ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}).

Note that

{z_{1}, …, z_{n}} ⊇ S_{1} ∩ S_{2} ⊇ V_{1} ∩ V_{2},

so that using the realizability requirement (see Def. 1), it is not too difficult to prove that for every j ≥ i_{0}:

(((L_{Φ_{1}} ∩ L_{Φ_{2}}, σ), j) ⊧ ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}).

That is

M ⊧ � � ready(z_{1} = c_{1} ∧ … ∧ z_{n} = c_{n}).

Theorem 7 The rule own (Fig. 2) is sound. That is, let Φ: ⟨V, Θ, ρ, E, S⟩ be an fsts, W ⊆ S be a set of variables, and p be an eltl formula. Then

(Φ ⊧ p) → ([own W. Φ] ⊧ p) .

Proof: Let Mown = (L, σ) be a [own W. Φ]-model. First, note that σ is a computation of [own W. Φ], so by Lemma 3 it is also a computation of Φ. Next, recall that for every j ≥ 0, L(σ(j)) is the set of all possible [own W. Φ]-successors of σ(j); but since Φ and [own W. Φ] have the same transition relation, L(σ(j)) is also the set of all possible Φ-successors of σ(j). Thus, Mown is a Φ-model, and by the assumption Mown ⊧ p.

Theorem 8 The axiom cont (Fig. 3) is valid. That is, let Φ: ⟨V, Θ, ρ, E, S⟩ be an fsts, and z be a controlled variable of Φ. Then

Φ ⊧ � � ready(z ≠ ⊥ ∧ S = ⊥) → � � (z ≠ ⊥).

Proof: (sketch) Suppose that M = (L, σ) is an Φ-model, and z ∈ C_{Φ}. σ is a computation of Φ, and is therefore fair w.r.t. z. The observant reader would notice that

� � ready(z ≠ ⊥ ∧ S = ⊥) → � � (z ≠ ⊥)

is simply a reformulation of the justice requirement w.r.t. z. From this it is not difficult to complete the proof. To prove the soundness of the comp, we need some preparation.

Definition 3 An eltl formula is called existential, if it does not contain ready or if each occurrence of ready appears under an even number of negations.

Lemma 9 Let M_{1} = (σ, L_{1}) and M_{2} = (σ, L_{2}) be two eltl models, s.t. L_{2}(σ(j)) ⊆ L_{1}(σ(j)), for each j = 0, 1, 2, . . .. Then, for every eltl formula p, and every i = 0, 1, 2, …:

1. ((M_{1}, i) ⊧ p ∧ (p is universal) → (M_{2}, i) ⊧ p) , and

2. ((M_{2}, i) ⊧ p ∧ (p is existential) → (M_{1}, i) ⊧ p) .

Proof: [(sketch)] The proof is carried out by mutual induction on the structure of p. Let us only mention that for the p = ¬(q) case, observe that if ¬(q) is universal then q is existential, and if ¬(q) is existential then q is universal. Hence, (1) follows from the induction hypothesis for (2), and vice-versa.

Theorem 10 The rule comp (Fig. 4) is sound. That is, let Φ_{1} and Φ_{2} be two compatible fsts modules, and p be a universal eltl formula. Then

(Φ ⊧ p) → (Φ_{1} ∥ Φ_{2} ⊧ p) .

Proof: Suppose M_{∥} = (L, σ) is a Φ_{1} ∥ Φ_{2}-model. By Lemma 5, the eltl model M_{1} = (L_{Φ}, σ), where L_{Φ_{1}}(s) = image(ρ_{Φ_{1}}, {s}), for every s ∈ Σ, is a Φ_{1}-model. So, by the assumption, M_{1} ⊧ p. Now, for every state s ∈ Σ:

L(s) = image(ρ_{Φ_{1}∥Φ_{2}}, {s}) ⊆ image(ρ_{Φ_{1}}, {s}) = L_{Φ_{1}}(s).

Hence, recall that p is universal, so that by using Lemma 9 (with M_{2} = M_{∥} and i = 0), we can conclude M_{∥} ⊧ p.

We conclude with a practical remark. Verification of fsts specification can be done by using existing symbolic model-checking algorithms. Computing the Lsets comes at no extra cost, since the predicate ready(p) is equivalent to the CTL formula EXp which every model checker knows how to compute very efficiently.

5 The fsts semantics of Signal

As mentioned in the introduction, the fsts model is a significant extension of the previous, more basic, αsts model [KP96] obtained by introducing operations (parallel composition and restriction) and by addressing fairness. The translation from Signal programs to corresponding fsts specifications, however, is not affected by these extensions, and can be carried out exactly as with αsts simply by taking the input/output variables as the externally observable variables and also as the synchronization variables. Nevertheless, to make the paper more self-contained, we present below the translation given by Kesten and Pnueli [KP96].

For a variable v, clocked(v) denotes the assertion:

clocked(v) : v ≠ ⊥

In the following, we describe how to construct an fsts Φ_{P} corresponding to a given Signal program P.

System Variables

The system variables of Φ are given by V = U ∪ X, where U are the Signal variables explicitly declared and manipulated in P, and X is a set of auxiliary variables. An auxiliary variable by the name of x.v is included in X for each expression of the form v $ appearing in P. For simplicity, we assume that the $ operator is only applied to variables and not to more general expressions. The value of x.v is intended to represent the value of v at the previous instance (present excluded) that v was different from ⊥.

Externally observable and synchronization variables

The externally observable variables E and also the synchronization variables S are those explicitly declared in P as input/output variables.

Initial Condition

The initial condition for Φ is given by

Θ: ⋀_{u∈U} u = ⊥ ∧ ⋀_{x.v∈U} x.v = ⊥

As will result from our fsts translation of Signal programs, they are all stuttering robust. Consequently, we can simplify things by assuming that the first state in each run of the system is a stuttering state.

Transition Relation

The transition relation ρ will be a conjunction of assertions, where each Signal statement gives rise to a conjunct in ρ.

We list the statements of Signal and, for each statement S, we present the conjunct contributed to ρ by S.

Basic Instructions

• Consider the Signal statement y := f(v_{1}, …, v_{n}), where f is a statefunction. Its contribution to ρ is given by:

clocked(y′) ≡ clocked(v′_{1}) ≡ … ≡ clocked(v′_{n})
∧ (clocked(y′) → y′ = f(v′_{1}, …, v′_{n}))

This formula requires that the signals y, v_{1}, …, v_{n} are present at precisely the same time instants, and that at these instants y = f(v_{1}, …, v_{n}).

• The contribution of the statement

y := v$ init v_{0}

is given by:

x′.v = if clocked(v′) then v′ else x.v
∧ y′ = ( \begin{matrix}if & ¬clocked(v′) & then & ⊥ \\ else if & x.v = ⊥ & then & v_{0} \\ else & x.v \end{matrix} )

The first conjunct of this formula defines the new value of x.v. If the new value of v is different from ⊥, then the new value of x.v is the new value of v. Otherwise, x.v retains its current value.

The second conjunct of the formula defines the new value of y by considering three cases. The first case requires that y′ = ⊥ whenever v′ = ⊥. This together with the other two cases implies that the clocks of v and y are identical. The second considered case is the first position at which v′ ≠ ⊥. Observe that the fact that we are at the else clause of the test ¬clocked(v′) implies that v′ ≠ ⊥, and that x.v = ⊥ implies that there was no previous position at which v ≠ ⊥. In this case, we take the new value of y (y′) to be v_{0}. The last case considers subsequent positions at which v′ ≠ ⊥. At all of these positions, y′ is taken to be the value of x.v, i.e., the value of v as it were at the previous (v′ ≠ ⊥)-position and as memorized in x.v.

• The contribution of the statement

y := v when b

is given by:

y′ = if (b′ = t) then v′ else ⊥.

• The contribution of the statement

y := u default v

is given by:

y′ = if clocked(u′) then u′ else v′.

Shorthand Instructions

• The contribution of the statement

φ(synchro v, y),

which states that v and y have the same clock, is given by:

clocked(v′) ≡ clocked(y′)

• The contribution of the statement

y := when(v),

which is an abbreviation for: y := v when v, for a boolean variable v, is given by:

y′ = if (v′ = t) then t else ⊥.

• The contribution of the statement

y := event(v),

which defines y to be a pure signal representing the clock of v, is given by:

y′ = if clocked(v′) then t else ⊥.

GUARD COUNT {input event fill, output boolean empty} =

synchro (when(zn = 0)), fill

| n :=  (10 when fill) default (zn − 1)
| zn :=  n $ init 0
| empty := when(n = 0) default (not fill)

Figure 5: A sample Signal program.

Example

In Fig. 5, we present a Signal program example, taken from [BGJ91]. We simplified the program to make it more self-contained. This small program models a system with a replenishable resource, for example, a water reservoir. The input event fill signals that that the reservoir is filled to the top. The local integer variable n measures the current water level. At each fill signal, the level is set to 10 (assumed maximal capacity). Then the level gradually decreases until it reaches 0. The output signal empty will register t when the water level drops to 0, and will register f when the reservoir is next filled.

The program as an fsts

The fsts translation of the Signal program of Fig. 5 is defined as follows: The system variables are given by:

V: \{\underbrace{fill, empty, zn, n}_{U}, \underbrace{x.n}_{X}\}.

The externally observable and synchronization variables are given by:

E = S: {fill, empty}.

The initial condition is given by:

Θ: fill = empty = zn = n = x.n = ⊥.

The transition relation ρ is given by:

(zn′ = 0) ≡ clocked(fill′)
∧  n′ = ( \begin{matrix}if & fill′ = t & then & 10 \\ else if & clocked(zn′) & then & zn′ − 1 \\ else & ⊥ \end{matrix} )
∧  x.n′ = if clocked(n′) then n′ else x.n
∧  zn′ = ( \begin{matrix}if & ¬clocked(n′) & then & ⊥ \\ else if & x.n = ⊥ & then & 0 \\ else & x.n \end{matrix} )

∧  empty′ = ( \begin{matrix}if & n′ = 0 & then & t \\ else if & fill′ = t & then & f \\ else & ⊥ \end{matrix} )

6 Conclusions and Future Work

We have presented fsts, a compositional semantics of synchronous systems that captures both safety and progress properties. We have motivated the fairness requirement and the operations of parallel composition and of restriction of variables by means of intuitive examples.

We have then introduced an extended version of linear temporal logic (eltl), in which it is convenient to express safety and liveness properties of synchronous specifications, and have presented (and demonstrated) a sound compositional proof system for it.

We have concluded by specifying how to translate programs written in an expressive representative of the synchronous school, namely Signal, to fsts.

Directions in future work which we intend to pursue are

• Specifying in detail the fsts semantics of Lustre, Esterel and Statecharts.

• Apply the deductive proof system developed here together with existing symbolic model-checking algorithms to the verification of fsts specifications that result from actual synchronous programs.

References

[AL95] M. Abadi and L. Lamport. Conjoining Specifications. TOPLAS, 17(3), pages 507–534, 1995.

[BGA97] A. Benveniste, P. Le Guernic, and P. Aubry. Compositionality in dataflow synchronous languages: specification & code generation. Proceedings of COMPOS’97.

[BGJ91] A. Benveniste, P. Le Guernic, and C. Jacquemot. Synchronous programming with event and relations: the SIGNAL language and its semantics. Science of Computer Programming, 16, pages 103– 149, 1991.

[BG92] G. Berry and G. Gonthier. The ESTEREL Synchronous Programming Language: Design, semantics, implementation. Science of Computer Programming, 19(2), 1992.

[CHPP87] P. Caspi, N. Halbwachs, D. Pilaud, and J. Plaice. LUSTRE, a Declarative Language for Programming Synchronous Systems. POPL’87, ACM Press, pages 178–188, 1987.

[H93] N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, Dordrecht, The Netherlands, 1993.

[Har87] D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8, pages 231–274, 1987.

[KP96] Y. Kesten and A. Pnueli. An αsts-based common semantics for signal and statecharts, March 1996. Sacres Manuscript.

[MP91] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

[Ow95] S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE trans. on software eng., 21(2), pages 107–125, 1995.

[PSS98] A. Pnueli, M. Siegel, and E. Singerman. Translation Validation. TACAS’98, LNCS, 1998.