Component-based systems can be modeled as black-box, standalone components, coordinated by an interaction protocol. In this paper we focus on developing reliable protocols, specified in a coordination language where their design, implementation, and property verification rely on the exact same model. In this context, to construct complex protocols compositionally, we use Reo, a powerful channel-based coordination language with well-defined semantics. We extend the current set of back-end languages supported by Reo's compiler with Promela, the specification language of the model checker SPIN. The automatic generation of Promela code from Reo specification enables system simulation and verification of LTL properties of Reo models using SPIN.
Development of a complex distributed system relies, generally, on assembling existing COTS (Commercial of-the-shelf) components (or services), such that their interactions after the composition manifest that of the required system. A major dificulty in developing such systems involves the correctness of the interaction protocol among their constituent heterogeneous components. As such, correct behavior of individual component is insuficient to imply the correctness of the composed system, because such system’s behavior depends on the protocol that coordinates its components. Precise specification and correctness of coordination protocols, thus, play a crucial role in construction of complex distributed systems.
Coordination languages, like Reo [
In this paper we propose to use Reo to guarantee a precise
speciifcation of complex protocols, and our main purpose is to propose
a formal approach for verifying their correctness. For that, we
propose to exploit the SPIN model checker [
Our choice of SPIN is motivated by the fact that it is one of the most employed model checkers, in both industrial and academic communities, for detecting software defects in concurrent system designs. SPIN has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft. In SPIN, a formal specification is built using Promela, which is an imperative language that resembles C in, .e.g, variable and type declaration.
To ensure the correctness of translation from Reo to Promela, we present suficient conditions to compile a protocol into a Promela program. We first introduce the notion of input/output designation, to direct the data flow in the protocol. Then, we define an environment as a set of processes that the protocol coordinates, and write the functional response of the protocol from the environment as a formula in guarded commands form. We finally present the translation of the guarded commands to Promela, to verify their LTL properties. We show the correctness of our translation by considering the behavior of the protocol specified in Reo and Promela. We demonstrate the relevance of our work in a case study involving design and verification of a railway component-based system.
Proofs of propositions and theorem are accessible at [
REO Reo is a channel-based coordination language used for compositional construction of coordinated systems. In this section, we explain the terminology used in Reo, together with a graphical syntax used to draw Reo circuit. We then present a logical syntax for representation of exogenous constraints. We define a guarded command form for logic formula, and use this structure to generate executable and verifiable code.
Terminology. The basic constructs in Reo consist of components, ports, channels and nodes. A port is a unidirectional means of synchronous exchange of data between two parties. Two operations can be performed on a port: put and get. The unidirectionality of a port means that each of the two parties on its two sides can use the port exclusively either as input or as output. A party that uses a port as output, can perform only put operations on that port, and a party that uses a port as input can perform only get operations on that port. A port fires whenever it has a get and a put operation pending on its respective sides. Firing of a port transfers the data item from the put operation to the get operation. A component is defined with a set of ports at its boundary, called its interface. Each port of an interface is either an input or an output port. When a port is shared by two components, we say that those two components are in composition. The port must be used as input in one component, and as output in the other component. A component can internally contain several components in composition, in which case we say that the component is composite. A component is called atomic if its behavior is defined in a specific formal semantic. A binary component, meaning that one whose interface consists of only two ports, is called a channel.
As pictured in Fig. 1, we represent graphically some standard
Reo component. More details can be found in [
Logical constraints. We can express the externally observable
behavior of a component as a relation over the sequences of data
items that it exchanges with its environment through its ports. In
this view, an interaction protocols is a relation that constrains the
exchanges of data among the ports of various components. We can
use logic formulas to express these constraints. We usually
separate two types of constraints. A synchronization constraint relates
ifring of ports, and a data constraint relates the values exchanged
among ports. We follow the work of [
We use D to denote the set of data items that flow through ports and are stored in memories. We use a special symbol ∗ < D, that represent no-data, to encode synchronization. We use D∗ to denote the set D ∪ {∗}. We use P to denote the set of variables that represent values exchanged through their homonym ports, M the set of variables that represent the current values stored in their homonym memory cells, and M ′ the set of variables that represent the next values to be stored in their unprimed homonym memory cells. We denote the set of variables as V , which consists of the union of P , M and M ′. Variables take their values from the domain D∗. Q and F respectively denote the set of n-ary predicate symbols and n-ary function symbol.
A term is either a variable v ∈ V (which can be a port or a memory variable), an n-ary function f ∈ F , or a constant d ∈ C (where C is the set of constant symbols).
t1,t2 ::= d | f (t1, ...,tn ) | v The set of term expression is denoted by E
A formula is built inductively by: ϕ ::= t1 = t2 |
B (t1, ...,tn ) | ϕ1 ∧ ϕ2 | ¬ϕ | ∃pϕ
Where B ∈ Q is a predicate symbol. The set of formula expressions is denoted by F . We use the shorthand notation t1 , t2 for ¬(t1 = t2), ⊥ for t1 , t1, and we get ϕ ∨ ψ = ¬(¬ϕ ∧ ¬ψ ) as well as ∀tϕ = ¬(∃t ¬ϕ) and ϕ =⇒ ψ = ¬ϕ ∨ ψ . Quantifiers range over port variables only. We call atomic a formula that is either an equality, an inequality, or a predicate. We call Vϕ the set of free variables occurring in ϕ. of terms J·K(Γ,γ ) : C ∪ F ∪ V inductively as:
Solution of constraints. We use γ : F → Dn ∗ → D∗, the interpretation function for function symbols, and Γ : V → D∗ to denote the interpretation function for variable symbols. We identify a constant c with its homonym value in D∗. We define the interpretation → D∗, over the functions Γ and γ , JdK(Γ,γ ) = d ∈ D∗ Jf (t1, ...,tn )K(Γ,γ ) = γ ( f ) (Jt1K(Γ,γ ) , ..., Jtn K(Γ,γ ) ) ∈ D∗ JvK(Γ,γ ) = Γ (v ) ∈ D∗
Each n-ary predicate symbol B ∈ Q is assumed to have an interpretation denoted by I (B), such that I (B) ⊆ Dn Given an in∗ terpretation function γ for the function symbols, a solution to a formula ϕ is an assignment Γ such that Γ satis f ies ϕ, written as Γ |= ϕ, defined inductively on ϕ as: Γ |= ⊤ always Γ |= t1 = t2 if Jt1K(Γ,γ ) = Jt2K(Γ,γ ) Γ |= ϕ1 ∧ ϕ2 if Γ |= ϕ1 and Γ |= ϕ2 Γ |= ¬ϕ if Γ ̸|= ϕ Γ |= ∃pϕ if there exists d ∈ D∗ such that Γ |= ϕ[d/p] Γ |= B (t1, ...,tn ) if (Jt1K(Γ,γ ) , ..., Jtn K(Γ,γ ) ) ∈ I (B)
We extend the domain definition of an n-ary function from to Dn∗ by defining f (t1, ...,tn ) = ∗ ⇐⇒ t1 = ∗ ∨ ... ∨ tn = ∗. 2.2
Components and permanent constraints. A Reo component, as introduced earlier, constrains the flow of data through its boundary ports. We call the logical formula used to represent this relation on the data flow through the ports of a component the permanent constraint of the component. Fig.1 shows several examples of permanent constraints of component.
Given a port p ∈ P , the proposition of whether or not p fires is encoded as an equality between p and elements of D∗. We say that p fires if p , ∗. On the other hand, p does not fire if p = ∗. Taking a,b ∈ P , we can now express that a and b fire synchronously, as the formula a = b.
Dn sync(a, b) fifo(a, b) a a • b b
a = b (m′ = a ∧ a , ∗ ∧ b = ∗ ∧ m = b) ∨ (m′ = a ∧ a = ∗ ∧ b , ∗ ∧ m = b) ∨ (m′ = m ∧ a = ∗ ∧ b = ∗)
The permanent constraint for a fifo channel has three clauses. The first one corresponds to filling the bufer with the data item observed at port a; the second one empties the bufer through port b; and the last one corresponds to the case where no port fires, in which case the value in the bufer must remain unchanged.
As hinted previously, protocols can be built by composing primitive. In the case of a composite component, the resulting permanent constraint is defined as the conjunction of the permanent constraints of the underlying components.
The logic is agnostic regarding the direction of data flow and merely represents the constraint on the data observed at each port. We introduce in the next paragraph the designation of input and output for variables, and the notion of ephemeral constraint.
I/O designation and ephemeral constraints. Given a formula, ϕ, and its set of variable Vϕ = P ∪ M ∪ M ′, we write the function io : Vϕ → {0, 1} as a designation for input and output variables such that: 1 v ∈ M io : v 7→ 0 v ∈ M ′ io(v ) ∈ {0, 1} v ∈ P We define V in as the set of variables v such that io(v ) = 1 and ϕ V out the set of variables such that io(v ) = 0. We also extend the ϕ notation to Pin and Pout , referring to the set of input and output port variables as designated by the io function.
Since a port is a shared entity between two components, we introduce the relative notion of environment for a component as the constraint imposed by the external world on its boundary ports. v ∈ V , i.e.:
[ Lϕ = τ ∈T a b ∗ ∗ {(σv1 , ...,σvN ) | σvi (t ) = τ (t ) (vi ) f or all vi ∈ V and t ∈ N} A component knows about the constraint imposed by the environment only by sensing the state of its boundary ports, and cannot access the permanent constraint that describes the environment. We model an environment ∆ by: v ∈ Pϕout ∩ P∆ ∗ ∆ : P∆ → D∗, v 7→ ∆ (v ) ∈ D∗ v ∈ Pϕin
where Pin ∩ P∆ = Pin , and Pout ∩ P∆ ⊆ Pout . We introduce the ϕ ϕ ϕ ϕ notion of ephemeral constraints ϵ and µ as opposed to a permanent constraint ϕ. In contrast to a permanent constraint, an ephemeral constraint may change in time. An environment ∆ imposes an external ephemeral constraint µ = Vv ∈P∆ (v = ∆ (v ) ∨ v = ∗) on the free variables of the permanent constraint ϕ of a component. The external ephemeral constraint µ represents the fact that, if the environment assigns ∗ to a variable, then the component does not have a choice but to assign ∗ to the same variable; however, if the environment has a data item pending at port v (described by the constraint ∆ (v ) , ∗), the component can still chose to assign ∗ to the variable and let the environment wait. An assignment Γ such that Γ |= ϕ imposes an internal ephemeral constraint on the next state of the component with ϵ = Vm ∈M (m = Γ (m′)). In other words, the next assignment Γ′ must then satisfy the constraint ϕ ∧ ϵ, where ϵ represents the internal state of the component, i.e., its memory values.
Intuitively, we can understand external ephemeral constraints as a current state of the ports on the boundary of a component (whether or not the environment has some I/O requests pending on a subset of ports), and the internal ephemeral constraint reflects the current state of the memory in a component. In composition with the permanent constraint, we get the current constraint of the component in the context of its internal and external states. 2.3
Operational semantic. Operationally, we consider formulas as labels for states, and assignments Γ as labels for transitions between states. Each state is labeled by an ephemeral constraint ϵ ∧ µ . We assume an initial state ϵ0 ∧ µ 0, given ϵ0 = Vm ∈M m = cm where cm ∈ D∗, and µ 0 = Vp ∈P p = ∗. In the initial state, the constraint µ 0 ensures that all port variables have the value ∗, and the constraint ϵ0 gives an initial value for all memory variables. We say that two states ϵ1 ∧ µ 1 and ϵ2 ∧ µ 2 under a permanent constraint ϕ are related by an assignment Γ if and only if Γ |= ϕ ∧ ϵ1 ∧ µ 1 and Γϕ ϵ2 = Vm ∈M (m = Γ (m′)). In this case, we write ϵ1 ∧ µ 1 −−→ ϵ2 ∧ µ 2, and drop the subscript ϕ when it is clear from the context.
Note that there exists an assignment Γ that relates each state with itself. Indeed, choosing the assignment Γ such that Γ (m) = Γ (m′) for all m ∈ M and Γ (p) = ∗ for all p ∈ P is a solution for any ephemeral constraint. Multiple distinct assignments may relate the same two states, in which case the labeled transition system contains multiple labeled edges between the same pair of states.
We refer to an infinite path in the labeled transition system ϵ1 ∧ µ 1 −−→ ϵ2 ∧ µ 2 −−→ ϵ3 ∧ µ 3 −−Γ→3 ... by the infinite sequence of its Γ1 Γ2 labels Γ1, Γ2, .... By T , we designate the set of infinite label sequences of the LTS. Given τ ∈ T , we write τ (i ) for the i-th assignment in the sequence τ , and τ (i ) (v ) for the value of the variable v ∈ Vϕ in the i-th assignment of the sequence τ .
Language of protocols. Analogously, an infinite sequence Γ0, Γ1, ... ∈ T can also be transformed into a tuple of data streams. For each variable v ∈ V , we define the data stream σv : N → D∗ such that σv (i ) = Γi (v ) for all i ∈ N. We call σV the tuple (σv1 ,σv2 , ...,σvN ) where {v1, ...,vN } = V
We define the language of a formula ϕ with initial memory values defined by ϵ0 as the set of tuples of data streams for the variables
Each component defines a constraint on the exchanges of data
items through its own boundary ports and two resulting time data
streams are shown in Fig. 2. This constraint is represented by a
formula such that the interpretation of the formula describes the
intended behavior of the component. We represent the behavior of
a component as a set of data streams, as also described in [
This overview sufices to understand the Reo compiler,
comprehend the behavior of independent components, and that of
composite components. In the next subsection, we explain the logical
form which the compiler uses to optimize the composition of
components. We define the notion of the guarded command form for a
formula, and relate it to code generation. The formal development
in the next subsection is supported by a tool [
Guarded commands. Given a formula ϕ representing a constraint, and an io designation, we define suficient conditions for ϕ to be written in the guarded command form. We first introduce a fragment of the logic of constraints, give some requirement on ϕ to be expressible as a guarded command, and show some properties if ϕ satisfied those requirements.
We denote by vin and vout a variable v such that io(v ) = 1 and io(v ) = 0, respectively. We denote a term by tin and tout such that: tin ::=
f (t1in , ...,tnin ) | d | The language of guards д is defined by the following grammar: tout ::= vout vin l ::= B (t1in , ...,tnin ) | t1in = t2in | tout = ∗ | ¬l д ::= l1 ∧ l2 The language of commands c is defined by the following grammar: We say that a formula ϕ is in guarded command form if c ::= tout = tin | c1 ∧ c2 ϕ = ^(дi =⇒ ci ) ∧ (_ дj ) i j where дi are formulas in the language of guards and ci are formulas in the language of commands. Given ϕ in guarded command form, we call an implication of the type д =⇒ c in ϕ, a guarded command of ϕ. We call the number of guarded commands in such a formula, the size of that formula. We denote the set of guards by G, and the set of commands by C.
We say that a quantifier free formula ϕ = ϕ1 ∨ ... ∨ ϕn in disjunctive normal form and expressed in the language of constraints is deterministic if ϕ can be written with the grammar of guarded commands such that ϕ = д1 ∧ c1 ∨ ... ∨ дn ∧ cn , where ∧ has precedence over ∨, дi are guards, ci are commands, and дi ∧ дj ≡ ⊥ for all i, j where i , j.
We assume that if a term tout is involved in an equality, then the other term is either ∗, or an input term tin . In other words, if an equality tout = t2out appears in the constraint ϕ, there must exist 1 an input term tin such that t1out = tin and t2out = tin . Moreover,
Proposition 1. A deterministic formula ϕ = д1 ∧c1 ∨ ... ∨дn ∧cn can be written as a guarded command where:
ϕ = (д1 =⇒ c1) ∧ ... ∧ (дn =⇒ cn ) ∧ (_ дi ) . as the formula:
Given two guarded commands ϕ = Vi (дi =⇒ ci ) ∧ (Wj дj ) and ψ = Vi (дi′ =⇒ ci′) ∧ (Wj дj′), we write the composition ϕ ∧ ψ ϕ ∧ ψ = ^(дi =⇒ ci ) ^(дi′ =⇒ ci′) ∧ (_ дi′ ∧ дj ) i i
i i,j
Proposition 2. Given two deterministic formulas ϕ and ψ , their product ϕ ∧ ψ is also deterministic.
As the construction in the proof of Proposition 2 shows, writing the composition of two deterministic formulas as a deterministic formula may increase the size of the resulting formula. Some optimizations that can be applied to formulas before forming their product, but we don’t detail them here for lack of
Example. We now consider an example of guarded commands for the fifo primitive. The fifo primitive has a permanent constraint written in Fig. 1, with the io designation of io(a) = 1 and io(b ) = 0, i.e., a is an input port and b is an output port. The formula of a fifo is deterministic, and with the result of Proposition 1, we can write its permanent constraint as a guarded command: ϕf if o =((a , ∗ ∧ b = ∗ ∧ m = ∗) =⇒ (m′ = a ∧ m = b )) ∧ ((a = ∗ ∧ b , ∗ ∧ m , ∗) =⇒ (m′ = a ∧ m = b )) ∧ ((a = ∗ ∧ b = ∗) =⇒
m′ = m) ∧ ((a , ∗ ∧ b = ∗ ∧ m = ∗) ∨ (a = ∗ ∧ b , ∗ ∧ m , ∗)∨ The formula for a fifo channel has two diferent guards. The first guard checks whether its source port a is active, in which case the command fills the bufer with the data observed at port a; the second guard checks whether the channel’s sink port b is active, in which case its command empties the bufer through port b.
Proposition 3. Given a deterministic formula ϕ in guarded command form, and an ephemeral constraint ϵ ∧ µ , Γ is a solution of ϕ ∧ ϵ ∧ µ if and only if there exists a unique guarded command д =⇒ c of ϕ such that:
Γ |= д ∧ ϵ ∧ µ and Γ |= c
We now look into the implementation and verification of a protocol described by a formula in guarded command form. As Proposition 3 shows, given a state of an environment and an internal state of our component, each solution is described by a unique guarded command. Therefore, given an environment and an internal state, a program implementing a protocol checks the set of guards that are satisfied by the state of the environment and the internal state, and nondeterministically satisfies one and only one corresponding command. We develop in the next section the steps leading from a protocol specification to a program written in Promela. (a = ∗ ∧ b = ∗))
In the previous section, we detailed the requirement and the procedure to write a protocol as a formula in the guarded command form. The implication of having such a form for a protocol makes it possible and easier to translate it into a program. In this section, we define a translation from a formula written as a guarded command to a Promela program. We show the correctness of the translation, by comparing the semantic of a Reo specification, and that of its target program in Promela.
Throughout this section, we assume a generic data type denoted as Data for data flowing in the protocol, since data type is specific in the application that employs the protocol.
Ports. In Reo, as defined in the previous section, a port is a
location where two components synchronize and exchange data. In
Promela, we implement a Reo port as a pair of two Promela
channels, each with a bufer size of one. We show that our Promela
implementation of a port simulates Reo’s synchronized message
passing between components.
typedef port {
chan data = [
As expressed in Listing 1, a port has a data channel and a synchronization channel. The data channel is responsible of the data lfow between input and output ends of a port. The Promela synch channel ensures synchronous exchange between these two ends.
As described in Listing 2, two actions can be performed on such a constructed port: put and take.
inline put(q,a) { int x; atomic{q.data!a; q.synch?x} } inline take(q,a) {
atomic{q.synch!-1; q.data?a} }
The action put has two arguments: a port q and a datum a. The function call put(q, a) atomically fills the data channel of q with the datum a, and blocks on the synch channel, waiting to synchronize with the component on the output side of q. The integer x is used to empty the synch channel, but its value does not matter.
The action take has a port q and a variable a as arguments. The function call take(q, a) atomically notifies, by filling the synch channel, that there is a component willing to take data, and blocks on the data channel, until a datum can be taken into the variable a. The integer value of −1 written into the synchronization channel is arbitrary, as synch is used only for signaling.
Environment. We call an external component that interacts with the main protocol, an aдent . For each port q in the protocol’s interface, we assume an aдent connected to that port. More precisely, if q is used as an input port by the protocol, the aдent connected to q must use q as an output port, and vice versa. We give in Listing 3 an example of a definition of an agent with two ports as its arguments. proctype agent(port p1; port p2){ /* p1: input, p2: output */ do
:: /* action */ od }
Each agent is defined as a proctype in Promela, and runs concurrently with the main protocol. We represent the generic behavior of an agent as an infinite sequence of non deterministic actions (with the do − od loop), but the definition of the precise behavior of an agent is left for the user. Since agents and protocol share ports, it is possible that an agent blocks until a datum is delivered at its port.
We assume a set of agents given by the user. Our compiler generates only the skeleton of an agent including the set of ports in its interface, with the direction of each port (either input or output). As an extension, we intend to make the input/output restriction of ports direction more strict, using the Promela assertion xr and xs to prevent misuse of port directionality. We later specify some properties of the desired observable behavior. 3.2
We define formally the translation of a formula written in guarded command form into a Promela specification.
Logical terms. Given a set of term expressions E, we define a mapping of E to a set of Promela specification P. We assume a function I that maps every constant, function, and predicate symbol to itthsaitnmtearppsreatatteiromn itno Paruomnieqluae. WnaemcealelxJp·KrEession in Promela, such : E → P the function that:
Jf (t1, ...,tn )KE = I ( f ) (Jt1KE , ..., Jtn KE ) JcKE = I (c ) JmKE = m
Jm′KE = m JpKE = p
Memory variables m and m′ are mapped to the same name in Promela, since they refer to the same memory location, subject to diferent actions.
Given a formula ϕ, its set of port variables P , and memory
variables M, the function : P ∪ M → P maps each port variable
p ∈ P and memory varJia·KbIle m ∈ M to a definition in Promela, such
that:
JpKI = port JpKE ; and JmKI = chan JmKE = [
Each port variable is mapped to an instance of the port structure in Promela. Every port name is unique, and given by JpKE . Each memory variable is defined as a channel of data type Data and of size 1. Every memory name is also unique, and given by m .
Besides the mapping of terms to Promela, we introduceJPrKoEmela vParaisabthlees ftuonacctcioensstfhoartmtauklaesvaarviaabrlieasb’levaelxuper.eWsseiounseanJd·KVretu:rEns→a
JmKV = _JmKE JpKV = _JpKE Jm′KV = _JmKE We use m p to refer to the current value in Promela of the memJorKyVvaarnidableKmV or of the port variable p.
J
Guarded commands. Because we have assumed the source formula to be deterministic, we define the target Promela program by induction on the syntax of the formula in guarded command form.
For a set of guards G, we define J·KG : G → P such that: Jд1 ∧ д2KG = Jд1KG &&Jд2KG J
Jt1in KV ==Jt2in KV Jt1in = t2in KG = empty(Jt1in KE ) true full(Jt1in KE .data) if t1in , ∗ ∧ t2in = ∗ J¬(t1in = t2in )KG = and t1in ∈ P !(Jt1in = t2in KG ) otherwise J¬(tout = ∗)KG = full( tout .synch)
J KE Note that guards of the shape p = ∗, where p ∈ Pin , are trivially mapped to true in Promela, since such condition can always be satisfied (a port could always have a silent behavior). However, guards of the shape ¬(p = ∗) must distinguish the case where p ∈ Pin , since the port p must have a pending input from the environment.
Before defining the translation from commands to Promela program, we must ensure that the conjunction is properly ordered. We consider the case where a memory variable m ∈ M is used as input and m′ ∈ M ′ as output in the same command. In this case, we first give precedence to the command involving m over the command involving m′, since m refers to the current value of m, and m′ refers to the new value of m. sucFhorthaast:et of commands C, we define the function J·KC : C → P Jc1 ∧ c2KC = Jc1KC ; Jc2KC ; Jtout = tin KC = (ptuotu(tJtou!t tKiEn,Jtin
J KE J KV
KV ) if tout ∈ P if tout ∈ M
The Promela program for a command is directly followed by an update of the state of the protocol. Since command execution consumes certain values from some port locations, we notify each input port involved in the command to release its value. Therefore, given a command c, for each tin occurring in c, we append at the end of itfhteinpr∈ogPraomr JJtciKnC th?eJtfionllowiinfgtisnta∈teMm e.nts: take(Jtin KE ,Jtin KV )
Given a determK Einistic KfoVrmula ϕ in the guarded command form, we inductively define the function J·KF : F → P such that:
Jд =⇒ cKF =JдKG -> atomic{JcKC }
The generic structure of a Promela program obtained from a
deterministic formula with n guarded commands is shown in Listing 4.
proctype Protocol(port p1;...){
/* p1: input, ... */
/* Memory declaration */
chan m = [
/* Guarded commands */ do :: (guard_1) ->
atomic{command_1} :: ... :: (guard_n) ->
atomic{command_n} od }
Example. We show as example the protocol of a fifo channel. The
corresponding deterministic formula for a fifo is presented in the
example in Section 2.4. Listing 5 shows the generated code obtained
from compiling the deterministic formula representing a fifo.
proctype Fifo(port a; port b){
/* a: input, b: output */
chan m = [
atomic{take(a,_a);m!_a;} :: (full(m) && full(b.synch)) ->
atomic{m?_m; put(b,_m);} od }
Note that the last guarded command is removed from the generated code, since it would result in the trivial statement: true -> atomic{m?_m;m!_m}, which essentially, merely copies the value of the memory m to itself.
Initialization. The init process in Promela defines the only active process in the initial state. Ports are initialized and shared between processes that run concurrently, i.e., we apply the instantiation function for all p ∈ P . We later reason on the set of processes in the initJp·KrIocess only. All agents and protocol are run concurrently.
Correctness. We use the semantic of Promela defined in [
Proposition 4. For every gv vector of global variable values, there exists an environment ∆ such that ∆ ≡ дv, and vice versa.
We use д =⇒ c to designate the translation of the guarded command Jд =⇒ cKtFo a Promela program. We denote the set of guarded commands as Sдc .
Theorem 5. Given a permanent constraint ϕ, where ϕ J KF is its translation, a state q = (l ,lv,дv ) and an environment ∆ such that дv ≡ ∆ , for every guarded command дc ∈ Sдc and a state q′ such дc that q −−→ q′, there exists an assignment such that Γ |= д ∧ c, where Jд =⇒ cKF = дc.
Completeness can be derived by showing that every solution of the guarded command corresponds to an implementation where the set of agents simulate the environment of the solution. By taking an implementation that unifies the agents, and using the nondeterministic properties of Promela, we can simulate any solution of the formula as a statement and a дv vector in Promela. Elaboration of this part remains as future work.
Adding our Promela code generator as a back-end for the Treo compiler significantly extends the application range of the current compiler. From the same Reo specification, the compiler can generate either an executable code in Java, or a verifiable code in Promela.
In this section, we consider specification of a railway protocol as a Reo circuit, its compilation into Promela, and verification of some of its properties using SPIN. 4.1
We consider the simplified trains protection in CBTC
(Communications Based Train Control) systems. The system is illustrated
in the Figure 3 and detailed in depth in previous work of one of
the author [
Event 1: sending coverage requests to MCU Event 2: T1 and T2 are covered Event 3: requesting VMAZs from MCU Event 4: VMAZs of T1 and T2 from MCU Event 5: computing VLMA
Wireless communication with T1 Velocity profile of T1
T1 s1 TEL
HEL s2
VLMA of T1 p1 s3
BTS Boundary between VMAZ1 and VMAZ2 s4 TEL
DEU
MCU Wireless communication with T2
T2
HEL
s5 s6
Trains path s7
Coverage area of MCU
The studied system consists of a set of components located inside and outside trains, that interact continuously to calculate and exchange parameters necessary to guarantee safe circulation of trains.
In this paper, we focus on modeling and verifying the interaction protocol of the main OBD component (On-Board Device) that interacts continuously with the Movement Control Unit component (MCU). This protocol implies constraints on the subcomponents of OBD (CtrVelocity, EmgcyBrake) and those of MCU (Coverage, ProdVmaz). Before modeling this protocol as a Reo circuit, in the next section, we describe it informally by showing the chaining of component actions that OBD and other components enable during their interactions.
The OBDs of T1 and T2 initiate the protection process by asking if they are visible to the MCU component, by sending the message covReq to Coverage subcomponent. There are several MCUs covering the entire line, with overlapping coverage sections, useful for information exchange between them. Locations are sent by wireless communication to the nearest Base Transmission Station (BTS) and saved in its Data Exchange Unit (DEU), which in turn transfers them to MCU (event 1). The internal subcomponent Coverage of MCU determines whether or not the zone between TEL and HEL (tail and head external locations ) is completely included within its coverage area, and responds to T1 and T2 by sending the messages covered or uncovered (event 2). Next, each train asks from its covering MCUs its Vital Movement Authority Zone (VMAZ), by sending the message vmazReq. A VMAZ is an area (sequence of segments) in which the train can safely circulate (event 3). MCU ensures that VMAZs of successive trains never overlap to avoid collisions. VMAZs are computed, by the MCU subcomponent ProdVmaz, through chaining of segments according to route information. Chaining terminates at the nearest obstacle on the train trajectory: the end of MCU coverage area, an uncontrolled switch, or the beginning of a segment containing TEL of the next train, etc. Finally, the train computes the Vital Limit of Movement Authority (VLMA) by incorporating a ifxed safety margin within the limit of its VMAZ (event 5).
Depending on VLMA an OBD component will either enable its
subcomponent CtrVelocity, or EmgcyBrake. The subcomponent
CtrVelocity gradually reduce the train velocity down to zero (via its
internal action ctrV elocity) before HEL reaches VLMA. The
activation of the subcomponent EmgcyBrake results into an emergency
brake action (emдcyBrake action).
The railway example presented above is translated into a Reo circuit,
described graphically in Fig. 4. Six diferent type of components are
used to model the protocol. Two fifo channels are used to represent
the asynchronous communication while Coverage sends an update
and expects an answer, and when Coverage communicates with
ProdVmaz. Transformer channels ComputeVlma and Update are
used to apply functions on the data flowing at their ports. Therefore,
the transformer ComputeVlma returns the speed value, responding
to the message sent by ProdVmaz, and Update updates the data of
the message sent by Coverage. The xrouter component (circle with
a cross) models the routing replication of data to CtrVelocity or
EmgcyBrake. Once a data enters the xrouter component, the data
is sent either to CtrVelocity or to EmergcyBrake but not to both.
Merger, replicator, and sync components have the usual behavior
and are used to model synchronization properties. For more details
on Reo components behavior, please refer to [
The protocol component (dashed line and grey font) represents the permanent constraint of the system. The four components CtrVelocity, EmgcyBrake, ProdVmaz, and Coverage, correspond to the environment of the protocol. In the next section, we generate the Promela code for this protocol, link the protocol with its agents, and verify some synchronization properties. 4.3
Initialization. To generate the Promela code corresponding to Reo circuit described in Fig. 4, we exploit our compiler that accepts as input Reo specification and generates as output Promela code by applying the rules described in Section 4. We obtain the following Promela proctypes described in Listing 6. init { port pcv; port pc1; port pc2; ... atomic{ run prodVmaz(ppv2,ppv1);run emergencyBrake(peb); run ctlVelocity(pcv); run coverture(pc2,pc3,pc1); run Protocol(pcv,pc3,pc1,ppv1,ppv2,pc2,peb) } }
Ports are first initialized with a respective unique named. Then, the Protocol proctype implements the Reo specification of the interaction protocol, with its corresponding interface. In addition, the proctypes ProdVmaz, EmgcyBrake, CtrlVelocity, Coverage, and EmgcyBrake implement the boundary agent, considered as an environment for the main protocol proctype. Each proctype accepts as parameters, ports associated with the interface of its respective component.
Protocol. In Listing 7, we show a partial implementation of the Protocol proctype corresponding to Reo specification described in Figure 4. To illustrate the result obtained from the compiler, we describe, for example, the actions coveReq, and covered, that are implemented as two guarded commands. The first action models the message sent by the OBD component to the agent Coverage. The second one models the message received by the OBD component from the agent Coverage. For example, as shown in Listing 7 in the implementation of coveReq, the guard part of the action specifies that the bufer m1 is full because there is a message to send, and the port pc2 (instantiation of the parameter p6 in Protocol) associated to the component Coverage is free. The command part of the action specifies that the message will be sent in Pc2 and the bufer will be available. proctype Protocol(port p1; ... ; port p7){ ... do ::(full(m1) && full(p6.sync)) -> atomic{ m1?_m1; put(p6,_m1);} /* covereq!*/ ... :: (full(p3.data) && empty(m2)) -> atomic{take(p3,_p3);m2!_p3;} /*covered*/ od }
Simulation and verification. The Promela program generated by
our compiler allows to run random or guided simulation with SPIN
for analyzing the protocol. It allows also to verify safety properties,
such as the absence of deadlock states. The verification performed
on the Promela program, corresponding to the case study, shows
that the protocol behavior does not reach any deadlock state. Using
the approach described in [
Flags. LTL properties, in our case, describe properties of the run in the generated code. As presented in previous section, the state of a generated Promela program is entirely captured in the global variables value, and a vector of local variables value for each concurrent proctype. We decide, to abstract system’s state by defining flags to describe the main state we interested in. As shown in Listing 8 /*flags declaration */ bit hassend=0, hasreceive=0, msg_covReq=0,msg_vmazReq=0, msg_covered=0, msg_uncovered=0, msg_vmaz=0,brake=0,ctrvelo=0; ... do ::(full(m1) && full(p6.sync)) -> atomic{ m1?_m1; put(p6,_m1); d_step{hassend=1; msg_covReq=1; hasreceive=0; msg_vmazReq=0; msg_covered=0; msg_uncovered=0; msg_vmaz=0; brake=0; ctrvelo=0;}} /* covereq!*/
Mainly, each sending and receiving action from the protocol point of view has a dedicated flag. This allows to keep track of the actions performed by the components and the reactions of their environment. These flags are updated together with each send/receive event, using a d_step statement to ensure the values assignment in one execution step. For example in Listing 8, we present the Promela code of the guarded command covereq enriched with its corresponding flags.
LTL properties. To verify the correctness of the specified protocol, we propose to verify the following LTL properties presented in Listing 9. ltl p1{[]((hassend==1 && msg_covReq==1) -> <> (hasreceive==1 && (msg_uncovered==1 || msg_covered==1)))} /*satified */ ltl p2{[](msg_covered==1 -> <> (hasreceive==1 && msg_vmaz==1 && brake==1))} /*not satisfied */
The property p1 specifies that, always if the component OBD sends the message covReq then it will receive a message covered or uncovered. This property is satisfied. The property p2 specifies that always if the OBD receives the message covered then it will receive the message vmaz and the action emдcyBrake will be enabled. This property is not satisfied, because there is the option of enabling the action ctrV elocity instead of emдcyBrake.
In this paper, we propose compiling Reo circuits into Promela to formally verify the LTL properties of protocols of interactions among components. Formal verification of Reo specifications using a number of tools has already appeared in the literature (see below). Complementing this existing set of tools, in our work, we opted to use the SPIN model checker, because (i) it is one of the most advanced analysis and verification tools available, and (ii) its Promela language resembles our guarded command formal specification of Reo circuits. We are not aware of a comprehensive work on verification of Reo circuits using SPIN.
We proposed a formal framework for translation of Reo models into Promela. We use a transition-systems-based operational semantics of Promela to express the formal semantics of Reo, through which we establish the correctness of our translation. Most of the existing work uses constraint automata, instead, as operational semantics.
Similar to our concerns, the CHARMY framework [
Vereofy [
The constraint automata semantics for Reo was also considered
in [
In this paper, we presented suficient conditions to compile a protocol specified in Reo into a program implemented in Promela. We introduced the notions of ephemeral and permanent constraints; the former consist of constraints that change through time, reflecting the states of the environment or internal memories, whereas the latter consist of structural constraints that must hold invariably. We defined suficient conditions for expressing the permanent constraint of a component in the guarded command form. We then defined a translation of a formula in guarded command form to a Promela program. We show the correctness of our translation, which we have implemented as a back-end for the current Reo compiler.
We demonstrate the relevance of our work in a case study involving design and verification of a railway component-based system. We use our compiler to translate the Reo specification of a protocol in this system into Promela, and use SPIN to verify LTL-specified properties, such as safety and liveness. In future work, we would like to support specification of LTL properties at design level as an extension of constraint formula. This direction is justified by the argument that in Reo, we can deduce the states of a protocol entirely from the current state of its boundary ports and its internal memory. A designer, thus, has enough information at the level of Reo to specify not just a protocol, but also its required LTL properties, in some suitable constraint language, which our extended compilation can subsequently translate into Promela LTL statement on protocol states, for verification.