=Paper=
{{Paper
|id=Vol-2245/modcomp_paper_5
|storemode=property
|title=Compiling Protocols to Promela and Verifying their LTL Properties
|pdfUrl=https://ceur-ws.org/Vol-2245/modcomp_paper_5.pdf
|volume=Vol-2245
|authors=Benjamin Lion,Samir Chouali,Farhad Arbab
|dblpUrl=https://dblp.org/rec/conf/models/LionCA18
}}
==Compiling Protocols to Promela and Verifying their LTL Properties==
https://ceur-ws.org/Vol-2245/modcomp_paper_5.pdf
Compiling Protocols to Promela and Verifying their LTL
Properties
Benjamin Lion Samir Chouali Farhad Arbab
Univ. Bourgogne Franche-Comté, CWI, Amesterdam, The Netherland
CWI, Amesterdam, The Netherland Farhad.Arbab@cwi.nl
B.Lion@cwi.nl FEMTO-ST Institute/CNRS, Besançon,
France
schouali@femto-st.fr
ABSTRACT exchanges, to the validation of intricate control software for inter-
Component-based systems can be modeled as black-box, stand- planetary spacecraft. In SPIN, a formal specification is built using
alone components, coordinated by an interaction protocol. In this Promela, which is an imperative language that resembles C in, .e.g,
paper we focus on developing reliable protocols, specified in a variable and type declaration.
coordination language where their design, implementation, and To ensure the correctness of translation from Reo to Promela, we
property verification rely on the exact same model. In this con- present sufficient conditions to compile a protocol into a Promela
text, to construct complex protocols compositionally, we use Reo, a program. We first introduce the notion of input/output designation,
powerful channel-based coordination language with well-defined to direct the data flow in the protocol. Then, we define an envi-
semantics. We extend the current set of back-end languages sup- ronment as a set of processes that the protocol coordinates, and
ported by Reo’s compiler with Promela, the specification language write the functional response of the protocol from the environment
of the model checker SPIN. The automatic generation of Promela as a formula in guarded commands form. We finally present the
code from Reo specification enables system simulation and verifi- translation of the guarded commands to Promela, to verify their
cation of LTL properties of Reo models using SPIN. LTL properties. We show the correctness of our translation by con-
sidering the behavior of the protocol specified in Reo and Promela.
KEYWORDS We demonstrate the relevance of our work in a case study involving
design and verification of a railway component-based system.
Component-based systems, Reo circuits, verification, Promela/SPIN Proofs of propositions and theorem are accessible at [1].
1 INTRODUCTION 2 REO
Development of a complex distributed system relies, generally, on Reo is a channel-based coordination language used for compo-
assembling existing COTS (Commercial off-the-shelf) components sitional construction of coordinated systems. In this section, we
(or services), such that their interactions after the composition man- explain the terminology used in Reo, together with a graphical
ifest that of the required system. A major difficulty in developing syntax used to draw Reo circuit. We then present a logical syntax
such systems involves the correctness of the interaction protocol for representation of exogenous constraints. We define a guarded
among their constituent heterogeneous components. As such, cor- command form for logic formula, and use this structure to generate
rect behavior of individual component is insufficient to imply the executable and verifiable code.
correctness of the composed system, because such system’s behav-
ior depends on the protocol that coordinates its components. Precise Terminology. The basic constructs in Reo consist of components,
specification and correctness of coordination protocols, thus, play ports, channels and nodes. A port is a unidirectional means of syn-
a crucial role in construction of complex distributed systems. chronous exchange of data between two parties. Two operations
Coordination languages, like Reo [3], offer powerful "glue-code" can be performed on a port: put and get. The unidirectionality of
to specify interaction protocols. Reo offers a non-traditional inter- a port means that each of the two parties on its two sides can use
action centric paradigm for design of concurrent system. It is a the port exclusively either as input or as output. A party that uses
coordination language, that supports exogenous composition of a port as output, can perform only put operations on that port, and
components and services via explicit, composable, pure interac- a party that uses a port as input can perform only get operations
tion specifications. The Reo model of a concurrent system consists on that port. A port fires whenever it has a get and a put operation
of a set of components that interact with each other through a pending on its respective sides. Firing of a port transfers the data
set of externally specified protocol constructs, called, connectors, item from the put operation to the get operation. A component is
that constrain synchronization and exchanges of data among those defined with a set of ports at its boundary, called its interface. Each
components. Primitive and complex connectors are specified in a port of an interface is either an input or an output port. When a
graphical or textual syntax [11]. Many semantic formalisms exist port is shared by two components, we say that those two compo-
for formal specification of the behavior of Reo connectors [14]. nents are in composition. The port must be used as input in one
In this paper we propose to use Reo to guarantee a precise speci- component, and as output in the other component. A component
fication of complex protocols, and our main purpose is to propose can internally contain several components in composition, in which
a formal approach for verifying their correctness. For that, we pro- case we say that the component is composite. A component is called
pose to exploit the SPIN model checker [13] to verify safety and atomic if its behavior is defined in a specific formal semantic. A
liveness properties of the specified protocols. binary component, meaning that one whose interface consists of
Our choice of SPIN is motivated by the fact that it is one of the only two ports, is called a channel.
most employed model checkers, in both industrial and academic As pictured in Fig. 1, we represent graphically some standard
communities, for detecting software defects in concurrent system Reo component. More details can be found in [3]. We define in the
designs. SPIN has been applied to everything from the verifica- next subsection a syntax to write the constraint relations among
tion of complex call processing software that is used in telephone the ports of a component. We later define a semantic of those
ModComp 2018, Oct 2018, Danemark Benjamin Lion, Samir Chouali, and Farhad Arbab
constraints as the set of data streams accepted by the constraint on Γ |= ϕ, defined inductively on ϕ as:
their respective ports of the component. Γ |= ⊤ always
Γ |= t 1 = t 2 iff Jt 1 K (Γ,γ ) = Jt 2 K (Γ,γ )
2.1 Exogenous constraints as formula Γ |= ϕ 1 ∧ ϕ 2 iff Γ |= ϕ 1 and Γ |= ϕ 2
Logical constraints. We can express the externally observable
behavior of a component as a relation over the sequences of data Γ |= ¬ϕ iff Γ ̸ |= ϕ
items that it exchanges with its environment through its ports. In Γ |= ∃pϕ iff there exists d ∈ D ∗ such that Γ |= ϕ[d/p]
this view, an interaction protocols is a relation that constrains the Γ |= B(t 1 , ...,tn ) iff (Jt 1 K (Γ,γ ) , ..., Jtn K (Γ,γ ) ) ∈ I (B)
exchanges of data among the ports of various components. We can
use logic formulas to express these constraints. We usually sepa- We extend the domain definition of an n-ary function from D n
rate two types of constraints. A synchronization constraint relates to D n∗ by defining f (t 1 , ...,tn ) = ∗ ⇐⇒ t 1 = ∗ ∨ ... ∨ tn = ∗.
firing of ports, and a data constraint relates the values exchanged
among ports. We follow the work of [10], where they used a spe- 2.2 Permanent and ephemeral constraints
cial data item NO-FLOW (that we represent here as ∗) to encode Components and permanent constraints. A Reo component, as
synchronization as data constraint. introduced earlier, constrains the flow of data through its boundary
We use D to denote the set of data items that flow through ports. We call the logical formula used to represent this relation
ports and are stored in memories. We use a special symbol ∗ < D, on the data flow through the ports of a component the perma-
that represent no-data, to encode synchronization. We use D ∗ to nent constraint of the component. Fig.1 shows several examples of
denote the set D ∪ {∗}. We use P to denote the set of variables that permanent constraints of component.
represent values exchanged through their homonym ports, M the Given a port p ∈ P, the proposition of whether or not p fires is
set of variables that represent the current values stored in their encoded as an equality between p and elements of D ∗ . We say that
homonym memory cells, and M ′ the set of variables that represent p fires if p , ∗. On the other hand, p does not fire if p = ∗. Taking
the next values to be stored in their unprimed homonym memory a,b ∈ P, we can now express that a and b fire synchronously, as
cells. We denote the set of variables as V , which consists of the the formula a = b.
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 sync(a, b) a =b
and n-ary function symbol. a b
A term is either a variable v ∈ V (which can be a port or a (m ′ = a ∧ a , ∗ ∧ b = ∗ ∧ m = b) ∨
memory variable), an n-ary function f ∈ F , or a constant d ∈ C fifo(a, b) • (m ′ = a ∧ a = ∗ ∧ b , ∗ ∧ m = b) ∨
a (m ′ = m ∧ a = ∗ ∧ b = ∗)
(where C is the set of constant symbols). b
t 1 ,t 2 ::= d | f (t 1 , ...,tn ) | v Figure 1: From left to right: textual syntax, graphical
syntax and permanent constraints. From top to bottom:
sync channel, and fifo channel.
The set of term expression is denoted by E
A formula is built inductively by:
The permanent constraint for a fifo channel has three clauses.
The first one corresponds to filling the buffer with the data item
ϕ ::= t 1 = t 2 | B(t 1 , ...,tn ) | ϕ1 ∧ ϕ2 | ¬ϕ | ∃pϕ observed at port a; the second one empties the buffer through port
b; and the last one corresponds to the case where no port fires, in
Where B ∈ Q is a predicate symbol. The set of formula expres- which case the value in the buffer must remain unchanged.
sions is denoted by F . We use the shorthand notation t 1 , t 2 for As hinted previously, protocols can be built by composing prim-
¬(t 1 = t 2 ), ⊥ for t 1 , t 1 , and we get ϕ ∨ ψ = ¬(¬ϕ ∧ ¬ψ ) as well itive. In the case of a composite component, the resulting perma-
as ∀tϕ = ¬(∃t¬ϕ) and ϕ =⇒ ψ = ¬ϕ ∨ ψ . Quantifiers range nent constraint is defined as the conjunction of the permanent
over port variables only. We call atomic a formula that is either an constraints of the underlying components.
equality, an inequality, or a predicate. We call Vϕ the set of free The logic is agnostic regarding the direction of data flow and
merely represents the constraint on the data observed at each port.
variables occurring in ϕ.
We introduce in the next paragraph the designation of input and
output for variables, and the notion of ephemeral constraint.
Solution of constraints. We use γ : F → D n∗ → D ∗ , the interpre-
tation function for function symbols, and Γ : V → D ∗ to denote I/O designation and ephemeral constraints. Given a formula, ϕ,
the interpretation function for variable symbols. We identify a con- and its set of variable Vϕ = P ∪ M ∪ M ′ , we write the function
stant c with its homonym value in D ∗ . We define the interpretation io : Vϕ → {0, 1} as a designation for input and output variables
of terms J·K (Γ,γ ) : C ∪ F ∪ V → D ∗ , over the functions Γ and γ , such that:
inductively as:
1
v∈M
io : v 7→ 0 v ∈ M′
JdK (Γ,γ ) = d ∈ D ∗ io(v) ∈ {0, 1} v ∈ P
Jf (t 1 , ...,tn )K (Γ,γ ) = γ ( f )(Jt 1 K (Γ,γ ) , ..., Jtn K (Γ,γ ) ) ∈ D ∗
We define Vϕin as the set of variables v such that io(v) = 1 and
JvK (Γ,γ ) = Γ(v) ∈ D ∗
Vϕout the set of variables such that io(v) = 0. We also extend the
notation to P in and P out , referring to the set of input and output
Each n-ary predicate symbol B ∈ Q is assumed to have an in- port variables as designated by the io function.
terpretation denoted by I (B), such that I (B) ⊆ D n∗ Given an in- Since a port is a shared entity between two components, we
terpretation function γ for the function symbols, a solution to a introduce the relative notion of environment for a component as
formula ϕ is an assignment Γ such that Γ satis f ies ϕ, written as the constraint imposed by the external world on its boundary ports.
Compiling Protocols to Promela and Verifying their LTL Properties ModComp 2018, Oct 2018, Danemark
A component knows about the constraint imposed by the environ- v ∈ V , i.e.:
ment only by sensing the state of its boundary ports, and cannot [
access the permanent constraint that describes the environment. Lϕ = {(σv1 , ...,σv N ) | σvi (t ) = τ (t )(vi ) f or all vi ∈ V and t ∈ N}
We model an environment ∆ by: τ ∈T
∗
v ∈ Pϕout ∩ P ∆
∆ : P ∆ → D ∗ , v 7→
∆(v) ∈ D ∗ v ∈ P in
a ∗ 1 1 ∗ ... a ∗ 1 ∗ 1 ...
ϕ b ∗ 1 1 ∗ ... b ∗ ∗ 1 ∗ ...
where Pϕin ∩ P ∆ = Pϕin , and Pϕout ∩ P ∆ ⊆ Pϕout . We introduce the
Figure 2: Examples of data streams on a ports a and b of a
notion of ephemeral constraints ϵ and µ as opposed to a permanent synchronous (left) and asynchronous (right) channel.
constraint ϕ. In contrast to a permanent constraint, an ephemeral
constraint may change in time. AnVenvironment ∆ imposes an
Each component defines a constraint on the exchanges of data
external ephemeral constraint µ = v ∈P ∆ (v = ∆(v) ∨ v = ∗) on
items through its own boundary ports and two resulting time data
the free variables of the permanent constraint ϕ of a component. streams are shown in Fig. 2. This constraint is represented by a
The external ephemeral constraint µ represents the fact that, if formula such that the interpretation of the formula describes the
the environment assigns ∗ to a variable, then the component does intended behavior of the component. We represent the behavior of
not have a choice but to assign ∗ to the same variable; however, if a component as a set of data streams, as also described in [11]. The
the environment has a data item pending at port v (described by symbol ∗ used in the table represents the case where no data flow
the constraint ∆(v) , ∗), the component can still chose to assign is observed at its respective port.
∗ to the variable and let the environment wait. An assignment Γ This overview suffices to understand the Reo compiler, compre-
such that Γ |= ϕ imposes an internal ephemeral constraint on the hend the behavior of independent components, and that of com-
next state of the component with ϵ = m ∈M (m = Γ(m ′ )). In other
V
posite components. In the next subsection, we explain the logical
words, the next assignment Γ ′ must then satisfy the constraint form which the compiler uses to optimize the composition of com-
ϕ ∧ ϵ, where ϵ represents the internal state of the component, i.e., ponents. We define the notion of the guarded command form for a
its memory values. formula, and relate it to code generation. The formal development
Intuitively, we can understand external ephemeral constraints in the next subsection is supported by a tool [2] developed at CWI.
as a current state of the ports on the boundary of a component Currently, the tool consists of a compilation suite from Treo, a tex-
(whether or not the environment has some I/O requests pending tual language for Reo [12], to executable code (Java) or verifiable
on a subset of ports), and the internal ephemeral constraint reflects code (Promela). We explain the formal steps in the compilation
the current state of the memory in a component. In composition process in the next subsection.
with the permanent constraint, we get the current constraint of the
component in the context of its internal and external states. 2.4 Compilation
2.3 Behavior and language of protocols The language of constraints expressed previously is not yet suf-
ficient to define compilation into a program. We need to restrict
Operational semantic. Operationally, we consider formulas as the expressiveness of the constraints such that we can compile
labels for states, and assignments Γ as labels for transitions between the resulting protocol into a program. We provide in this section
states. Each state is labeled by an ephemeral Vconstraint ϵ ∧ µ. We a restriction of the language of constraints and define a generic
V ϵ0 ∧ µ 0 , given ϵ0 = m ∈M m = cm where
assume an initial state constraint solver for it.
cm ∈ D ∗ , and µ 0 = p ∈P p = ∗. In the initial state, the constraint µ 0
Guarded commands. Given a formula ϕ representing a constraint,
ensures that all port variables have the value ∗, and the constraint
and an io designation, we define sufficient conditions for ϕ to be
ϵ0 gives an initial value for all memory variables. We say that two
written in the guarded command form. We first introduce a frag-
states ϵ1 ∧ µ 1 and ϵ2 ∧ µ 2 under a permanent constraint ϕ are
ment of the logic of constraints, give some requirement on ϕ to be
related by an assignment Γ if and only if Γ |= ϕ ∧ ϵ1 ∧ µ 1 and
Γϕ
expressible as a guarded command, and show some properties if ϕ
ϵ2 = m ∈M (m = Γ(m ′ )). In this case, we write ϵ1 ∧ µ 1 −−→ ϵ2 ∧ µ 2 , satisfied those requirements.
V
and drop the subscript ϕ when it is clear from the context. We denote by v in and v out a variable v such that io(v) = 1 and
Note that there exists an assignment Γ that relates each state with io(v) = 0, respectively. We denote a term by t in and t out such that:
itself. Indeed, choosing the assignment Γ such that Γ(m) = Γ(m ′ )
t in ::= d | f (t 1in , ...,tnin ) | v in t out ::= v out
for all m ∈ M and Γ(p) = ∗ for all p ∈ P is a solution for any
ephemeral constraint. Multiple distinct assignments may relate The language of guards д is defined by the following grammar:
l ::= B(t 1in , ...,tnin ) | t 1in = t 2in | t out = ∗ | ¬l
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 д ::= l 1 ∧ l 2
Γ1 Γ2 Γ3 The language of commands c is defined by the following grammar:
ϵ1 ∧ µ 1 −−→ ϵ2 ∧ µ 2 −−→ ϵ3 ∧ µ 3 −−→ ... by the infinite sequence of its
labels Γ1 , Γ2 , .... By T , we designate the set of infinite label sequences c ::= t out = t in | c 1 ∧ c 2
of the LTS. Given τ ∈ T , we write τ (i) for the i-th assignment in We say that a formula ϕ is in guarded command form if
the sequence τ , and τ (i)(v) for the value of the variable v ∈ Vϕ in ^ _
the i-th assignment of the sequence τ . ϕ= (дi =⇒ c i ) ∧ ( дj )
i j
Language of protocols. Analogously, an infinite sequence Γ0 , Γ1 , ... ∈
T can also be transformed into a tuple of data streams. For each where дi are formulas in the language of guards and c i are formulas
variable v ∈ V , we define the data stream σv : N → D ∗ such that in the language of commands. Given ϕ in guarded command form,
σv (i) = Γi (v) for all i ∈ N. We call σV the tuple (σv1 ,σv2 , ...,σv N ) we call an implication of the type д =⇒ c in ϕ, a guarded command
where {v 1 , ...,v N } = V of ϕ. We call the number of guarded commands in such a formula,
We define the language of a formula ϕ with initial memory values the size of that formula. We denote the set of guards by G, and the
defined by ϵ0 as the set of tuples of data streams for the variables set of commands by C.
ModComp 2018, Oct 2018, Danemark Benjamin Lion, Samir Chouali, and Farhad Arbab
We say that a quantifier free formula ϕ = ϕ 1 ∨ ... ∨ ϕn in dis- 3 FROM REO TO PROMELA
junctive normal form and expressed in the language of constraints In the previous section, we detailed the requirement and the pro-
is deterministic if ϕ can be written with the grammar of guarded cedure to write a protocol as a formula in the guarded command
commands such that ϕ = д1 ∧ c 1 ∨ ... ∨ дn ∧ c n , where ∧ has prece- form. The implication of having such a form for a protocol makes it
dence over ∨, дi are guards, c i are commands, and дi ∧ дj ≡ ⊥ for possible and easier to translate it into a program. In this section, we
all i, j where i , j. define a translation from a formula written as a guarded command
We assume that if a term t out is involved in an equality, then to a Promela program. We show the correctness of the translation,
the other term is either ∗, or an input term t in . In other words, if an by comparing the semantic of a Reo specification, and that of its
equality t 1out = t 2out appears in the constraint ϕ, there must exist target program in Promela.
an input term t in such that t 1out = t in and t 2out = t in . Moreover,
Throughout this section, we assume a generic data type denoted
as Data for data flowing in the protocol, since data type is specific
Proposition 1. A deterministic formula ϕ = д1 ∧c 1 ∨ ... ∨дn ∧c n in the application that employs the protocol.
can be written as a guarded command where:
_ 3.1 Ports and environment in Promela
ϕ = (д1 =⇒ c 1 ) ∧ ... ∧ (дn =⇒ c n ) ∧ ( дi ) Ports. In Reo, as defined in the previous section, a port is a lo-
i cation where two components synchronize and exchange data. In
. Promela, we implement a Reo port as a pair of two Promela chan-
Given two guarded commands ϕ = i (дi =⇒ c i ) ∧ ( j дj )
V W
nels, each with a buffer size of one. We show that our Promela
and ψ = i (дi =⇒ c i ) ∧ ( j дj ), we write the composition ϕ ∧ ψ
V ′ ′ W ′ implementation of a port simulates Reo’s synchronized message
passing between components.
as the formula:^ ^ _ typedef port {
ϕ ∧ψ = (дi =⇒ c i ) (дi′ =⇒ c i′ ) ∧ ( дi′ ∧ дj ) chan data = [1] of {Data};
i i i,j chan synch = [1] of {int}; }
Listing 1: definition of a Reo port in Promela
Proposition 2. Given two deterministic formulas ϕ and ψ , their
product ϕ ∧ ψ is also deterministic. As expressed in Listing 1, a port has a data channel and a syn-
chronization channel. The data channel is responsible of the data
As the construction in the proof of Proposition 2 shows, writing flow between input and output ends of a port. The Promela synch
the composition of two deterministic formulas as a deterministic channel ensures synchronous exchange between these two ends.
formula may increase the size of the resulting formula. Some op- As described in Listing 2, two actions can be performed on such
timizations that can be applied to formulas before forming their a constructed port: put and take.
product, but we don’t detail them here for lack of
inline put(q,a) { inline take(q,a) {
Example. We now consider an example of guarded commands int x; atomic{q.synch!-1; q.data?a} }
for the fifo primitive. The fifo primitive has a permanent constraint atomic{q.data!a;
written in Fig. 1, with the io designation of io(a) = 1 and io(b) = 0, q.synch?x} }
i.e., a is an input port and b is an output port. The formula of a fifo
Listing 2: put and take functions
is deterministic, and with the result of Proposition 1, we can write
its permanent constraint as a guarded command: The action put has two arguments: a port q and a datum a. The
ϕ f if o =((a , ∗ ∧ b = ∗ ∧ m = ∗) =⇒ (m ′ = a ∧ m = b)) ∧ 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
((a = ∗ ∧ b , ∗ ∧ m , ∗) =⇒ (m ′ = a ∧ m = b)) ∧ with the component on the output side of q. The integer x is used
((a = ∗ ∧ b = ∗) =⇒ m ′ = m) ∧ to empty the synch channel, but its value does not matter.
The action take has a port q and a variable a as arguments.
((a , ∗ ∧ b = ∗ ∧ m = ∗) ∨ (a = ∗ ∧ b , ∗ ∧ m , ∗)∨ The function call take(q, a) atomically notifies, by filling the synch
(a = ∗ ∧ b = ∗)) channel, that there is a component willing to take data, and blocks
The formula for a fifo channel has two different guards. The first on the data channel, until a datum can be taken into the variable a.
The integer value of −1 written into the synchronization channel
guard checks whether its source port a is active, in which case
the command fills the buffer with the data observed at port a; the is arbitrary, as synch is used only for signaling.
second guard checks whether the channel’s sink port b is active, in Environment. We call an external component that interacts with
which case its command empties the buffer through port b. the main protocol, an aдent. For each port q in the protocol’s inter-
face, we assume an aдent connected to that port. More precisely, if
Proposition 3. Given a deterministic formula ϕ in guarded com- q is used as an input port by the protocol, the aдent connected to q
mand form, and an ephemeral constraint ϵ ∧ µ, Γ is a solution of must use q as an output port, and vice versa. We give in Listing 3 an
ϕ ∧ ϵ ∧ µ if and only if there exists a unique guarded command example of a definition of an agent with two ports as its arguments.
д =⇒ c of ϕ such that:
Γ |= д ∧ ϵ ∧ µ and Γ |= c proctype agent(port p1; port p2){
/* p1: input, p2: output */
We now look into the implementation and verification of a proto- do
:: /* action */
col described by a formula in guarded command form. As Proposi- od }
tion 3 shows, given a state of an environment and an internal state Listing 3: A generic structure for an agent
of our component, each solution is described by a unique guarded
command. Therefore, given an environment and an internal state, Each agent is defined as a proctype in Promela, and runs concur-
a program implementing a protocol checks the set of guards that rently with the main protocol. We represent the generic behavior of
are satisfied by the state of the environment and the internal state, an agent as an infinite sequence of non deterministic actions (with
and nondeterministically satisfies one and only one corresponding the do − od loop), but the definition of the precise behavior of an
command. We develop in the next section the steps leading from a agent is left for the user. Since agents and protocol share ports, it is
protocol specification to a program written in Promela. possible that an agent blocks until a datum is delivered at its port.
Compiling Protocols to Promela and Verifying their LTL Properties ModComp 2018, Oct 2018, Danemark
We assume a set of agents given by the user. Our compiler gen- Before defining the translation from commands to Promela pro-
erates only the skeleton of an agent including the set of ports in its gram, we must ensure that the conjunction is properly ordered. We
interface, with the direction of each port (either input or output). consider the case where a memory variable m ∈ M is used as input
As an extension, we intend to make the input/output restriction and m ′ ∈ M ′ as output in the same command. In this case, we first
of ports direction more strict, using the Promela assertion xr and give precedence to the command involving m over the command
xs to prevent misuse of port directionality. We later specify some involving m ′ , since m refers to the current value of m, and m ′ refers
properties of the desired observable behavior. to the new value of m.
For a set of commands C, we define the function J·K C : C → P
3.2 Translation of a Reo specification such that:
We define formally the translation of a formula written in guarded
command form into a Promela specification. Jc 1 ∧ c 2 K C = Jc 1 K C ; Jc 2 K C ;
put(Jt out K E ,Jt in K V ) if t out ∈ P
(
Logical terms. Given a set of term expressions E, we define a Jt out = t in K C =
mapping of E to a set of Promela specification P. We assume a func- Jt out K E !Jt in K V if t out ∈ M
tion I that maps every constant, function, and predicate symbol to
its interpretation in Promela. We call J·K E : E → P the function The Promela program for a command is directly followed by an
that maps a term to a unique name expression in Promela, such update of the state of the protocol. Since command execution con-
that: sumes certain values from some port locations, we notify each input
port involved in the command to release its value. Therefore, given
Jf (t 1 , ...,tn )K E = I ( f )(Jt 1 K E , ..., Jtn K E ) a command c, for each t in occurring in c, we append at the end of
JcK E = I (c) JmK E = m the program JcK C the following statements: take(Jt in K E ,Jt in K V )
′
Jm K E = m JpK E = p if t in ∈ P or Jt in K E ?Jt in K V if t in ∈ M.
Given a deterministic formula ϕ in the guarded command form,
Memory variables m and m ′ are mapped to the same name in we inductively define the function J·K F : F → P such that:
Promela, since they refer to the same memory location, subject to
different actions. Jд =⇒ cK F =JдK G -> atomic{JcK C }
Given a formula ϕ, its set of port variables P, and memory vari-
ables M, the function J·K I : P ∪ M → P maps each port variable The generic structure of a Promela program obtained from a deter-
p ∈ P and memory variable m ∈ M to a definition in Promela, such ministic formula with n guarded commands is shown in Listing 4.
that:
JpK I = port JpK E ; and JmK I = chan JmK E = [1] of {Data}; proctype Protocol(port p1;...){
/* p1: input, ... */ /* Guarded commands */
Each port variable is mapped to an instance of the port structure /* Memory declaration */ do
chan m = [1] of {int}; :: (guard_1) ->
in Promela. Every port name is unique, and given by JpK E . Each /* Initial state */ atomic{command_1}
memory variable is defined as a channel of data type Data and of m!0; :: ...
size 1. Every memory name is also unique, and given by JmK E . /* Local variables */ :: (guard_n) ->
Besides the mapping of terms to Promela, we introduce Promela int _m; int _p1 ; atomic{command_n}
... od }
variables to access formula variables’ value. We use J·K V : E →
P as the function that takes a variable expression and returns a Listing 4: a generic structure of a protocol
Promela expression such that:
JmK V = _JmK E JpK V = _JpK E Jm ′ K V = _JmK E
Example. We show as example the protocol of a fifo channel. The
We use JmK V and JpK V to refer to the current value in Promela of corresponding deterministic formula for a fifo is presented in the
the memory variable m or of the port variable p. example in Section 2.4. Listing 5 shows the generated code obtained
Guarded commands. Because we have assumed the source for- from compiling the deterministic formula representing a fifo.
mula to be deterministic, we define the target Promela program by proctype Fifo(port a; port b){
induction on the syntax of the formula in guarded command form. /* a: input, b: output */
For a set of guards G, we define J·K G : G → P such that: chan m = [1] of {int};
int _m; int _a ; int _b ;
Jд1 ∧ д2 K G = Jд1 K G &&Jд2 K G do
JB(t 1in , ...,tnin )K G = I (B)(Jt 1in K V , ..., Jtnin K V )
:: (empty(m) && full(a.data)) ->
atomic{take(a,_a);m!_a;}
in in if t 1in , ∗ ∧ t 2in , ∗ :: (full(m) && full(b.synch)) ->
Jt 1 K V ==Jt
2 KV atomic{m?_m; put(b,_m);}
Jt 1in = t 2in K G = in K ) if t 1in , ∗ ∧ t 2in = ∗ and t 1in ∈ M
empty(Jt 1 E od }
true
otherwise Listing 5: Promela code generated for a Reo fifo channel
full(Jt 1in K E .data) if t 1in , ∗ ∧ t 2in = ∗ with a String buffer
J¬(t 1in = t 2in )K G = and t 1in ∈ P
in in Note that the last guarded command is removed from the gener-
!(Jt 1 = t 2 K G )
otherwise ated code, since it would result in the trivial statement: true ->
J¬(t out = ∗)K G = full(Jt out K E .synch) atomic{m?_m;m!_m}, which essentially, merely copies the value of
the memory m to itself.
Note that guards of the shape p = ∗, where p ∈ P in , are trivially
mapped to true in Promela, since such condition can always be Initialization. The init process in Promela defines the only active
satisfied (a port could always have a silent behavior). However, process in the initial state. Ports are initialized and shared between
guards of the shape ¬(p = ∗) must distinguish the case where processes that run concurrently, i.e., we apply the instantiation
p ∈ P in , since the port p must have a pending input from the function J·K I for all p ∈ P. We later reason on the set of processes
environment. in the init process only. All agents and protocol are run concurrently.
ModComp 2018, Oct 2018, Danemark Benjamin Lion, Samir Chouali, and Farhad Arbab
Correctness. We use the semantic of Promela defined in [21] to
show the correctness of our translation. The operational semantics
of a Promela program P composed of processes Pi is defined as a
graphT = (Q, →,q 0 ) where Q is a set of states and → is a binary rela-
tion on states. A state q ∈ Q is a tuple q = (l 0 , ...,lm ,lv1, ...,lvm,дv)
where each li is a location in process Pi , lvi is the vector of local
variable values in process Pi , and дv is the vector of global variables
in P. The state s 0 ∈ Q refers to the initial state.
Proposition 4. For every gv vector of global variable values, there
exists an environment ∆ such that ∆ ≡ дv, and vice versa.
We use Jд =⇒ cK F to designate the translation of the guarded
command д =⇒ c to a Promela program. We denote the set of
guarded commands as Sдc .
Theorem 5. Given a permanent constraint ϕ, where JϕK F 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д =⇒ cK F = дc.
Figure 4: Reo circuit
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 non- In this paper, we focus on modeling and verifying the interac-
deterministic properties of Promela, we can simulate any solution of tion protocol of the main OBD component (On-Board Device) that
the formula as a statement and a дv vector in Promela. Elaboration interacts continuously with the Movement Control Unit component
of this part remains as future work. (MCU). This protocol implies constraints on the subcomponents
Adding our Promela code generator as a back-end for the Treo of OBD (CtrVelocity, EmgcyBrake) and those of MCU (Coverage,
compiler significantly extends the application range of the cur- ProdVmaz). Before modeling this protocol as a Reo circuit, in the
rent compiler. From the same Reo specification, the compiler can next section, we describe it informally by showing the chaining of
generate either an executable code in Java, or a verifiable code in component actions that OBD and other components enable during
Promela. their interactions.
The OBDs of T1 and T2 initiate the protection process by asking
4 CASE STUDY if they are visible to the MCU component, by sending the message
In this section, we consider specification of a railway protocol as a covReq to Coverage subcomponent. There are several MCUs cover-
Reo circuit, its compilation into Promela, and verification of some ing the entire line, with overlapping coverage sections, useful for
of its properties using SPIN. information exchange between them. Locations are sent by wireless
communication to the nearest Base Transmission Station (BTS) and
4.1 Railway case study saved in its Data Exchange Unit (DEU), which in turn transfers them
We consider the simplified trains protection in CBTC (Communi- to MCU (event 1). The internal subcomponent Coverage of MCU
cations Based Train Control) systems. The system is illustrated determines whether or not the zone between TEL and HEL (tail and
in the Figure 3 and detailed in depth in previous work of one of head external locations ) is completely included within its coverage
the author [19]. To illustrate our approach, we propose a slight area, and responds to T1 and T2 by sending the messages covered or
adaptation of the original version of the system. 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
Event 1: sending coverage requests to MCU train can safely circulate (event 3). MCU ensures that VMAZs of
Event 2: T1 and T2 are covered
Event 3: requesting VMAZs from MCU
DEU
MCU successive trains never overlap to avoid collisions. VMAZs are com-
Event 4: VMAZs of T1 and T2 from MCU
Event 5: computing VLMA puted, by the MCU subcomponent ProdVmaz, through chaining of
Wireless communication with T2
BTS
segments according to route information. Chaining terminates at
Wireless communication with T1 Boundary between
VMAZ1 and VMAZ2
the nearest obstacle on the train trajectory: the end of MCU cov-
s4 TEL
T2
HEL s5 s6
erage area, an uncontrolled switch, or the beginning of a segment
Trains path containing TEL of the next train, etc. Finally, the train computes
Velocity profile of T1
the Vital Limit of Movement Authority (VLMA) by incorporating a
s3
VLMA of T1
fixed safety margin within the limit of its VMAZ (event 5).
TEL
T1
HEL s2 s7
Depending on VLMA an OBD component will either enable its
s1 p1
Coverage area of MCU
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 activa-
Figure 3: Simplified trains protection functions. tion of the subcomponent EmgcyBrake results into an emergency
brake action (emдcyBrake action).
The studied system consists of a set of components located in-
side and outside trains, that interact continuously to calculate and 4.2 Reo specification
exchange parameters necessary to guarantee safe circulation of The railway example presented above is translated into a Reo circuit,
trains. described graphically in Fig. 4. Six different type of components are
Compiling Protocols to Promela and Verifying their LTL Properties ModComp 2018, Oct 2018, Danemark
used to model the protocol. Two fifo channels are used to represent od }
the asynchronous communication while Coverage sends an update Listing 7: Guarded commands for covereq and covered ac-
and expects an answer, and when Coverage communicates with tions
ProdVmaz. Transformer channels ComputeVlma and Update are
used to apply functions on the data flowing at their ports. Therefore,
Simulation and verification. The Promela program generated by
the transformer ComputeVlma returns the speed value, responding
our compiler allows to run random or guided simulation with SPIN
to the message sent by ProdVmaz, and Update updates the data of
for analyzing the protocol. It allows also to verify safety properties,
the message sent by Coverage. The xrouter component (circle with such as the absence of deadlock states. The verification performed
a cross) models the routing replication of data to CtrVelocity or on the Promela program, corresponding to the case study, shows
EmgcyBrake. Once a data enters the xrouter component, the data that the protocol behavior does not reach any deadlock state. Using
is sent either to CtrVelocity or to EmergcyBrake but not to both. the approach described in [9], we define, in the next subsection,
Merger, replicator, and sync components have the usual behavior some new flag variables used to verify liveness properties. The ex-
and are used to model synchronization properties. For more details periment detailed in the use case can be reproduced by downloading
on Reo components behavior, please refer to [3]. the Reo compiler [2].
The protocol component (dashed line and grey font) represents
the permanent constraint of the system. The four components 4.4 Verification of LTL properties
CtrVelocity, EmgcyBrake, ProdVmaz, and Coverage, correspond to
the environment of the protocol. In the next section, we generate Flags. LTL properties, in our case, describe properties of the
the Promela code for this protocol, link the protocol with its agents, run in the generated code. As presented in previous section, the
and verify some synchronization properties. 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
4.3 Code generation defining flags to describe the main state we interested in. As shown
Initialization. To generate the Promela code corresponding to in Listing 8
Reo circuit described in Fig. 4, we exploit our compiler that accepts
/*flags declaration */
as input Reo specification and generates as output Promela code by bit hassend=0, hasreceive=0, msg_covReq=0,msg_vmazReq=0,
applying the rules described in Section 4. We obtain the following msg_covered=0, msg_uncovered=0, msg_vmaz=0,brake=0,ctrvelo=0;
Promela proctypes described in Listing 6. ...
do
init { ::(full(m1) && full(p6.sync)) -> atomic{ m1?_m1; put(p6,_m1);
port pcv; port pc1; port pc2; d_step{hassend=1; msg_covReq=1; hasreceive=0; msg_vmazReq=0;
... msg_covered=0; msg_uncovered=0; msg_vmaz=0; brake=0;
atomic{ ctrvelo=0;}} /* covereq!*/
run prodVmaz(ppv2,ppv1);run emergencyBrake(peb);
run ctlVelocity(pcv); run coverture(pc2,pc3,pc1);
Listing 8: Flags of the generated code
run Protocol(pcv,pc3,pc1,ppv1,ppv2,pc2,peb) } }
Mainly, each sending and receiving action from the protocol point
Listing 6: Generated proctypes of view has a dedicated flag. This allows to keep track of the actions
performed by the components and the reactions of their environ-
Ports are first initialized with a respective unique named. Then, ment. These flags are updated together with each send/receive
the Protocol proctype implements the Reo specification of the event, using a d_step statement to ensure the values assignment
interaction protocol, with its corresponding interface. In addition, in one execution step. For example in Listing 8, we present the
the proctypes ProdVmaz, EmgcyBrake, CtrlVelocity, Coverage, Promela code of the guarded command covereq enriched with its
and EmgcyBrake implement the boundary agent, considered as corresponding flags.
an environment for the main protocol proctype. Each proctype LTL properties. To verify the correctness of the specified protocol,
accepts as parameters, ports associated with the interface of its we propose to verify the following LTL properties presented in
respective component. Listing 9.
Protocol. In Listing 7, we show a partial implementation of the ltl p1{[]((hassend==1 && msg_covReq==1) -> <> (hasreceive==1
Protocol proctype corresponding to Reo specification described && (msg_uncovered==1 || msg_covered==1)))} /*satified */
in Figure 4. To illustrate the result obtained from the compiler, we ltl p2{[](msg_covered==1 -> <> (hasreceive==1 && msg_vmaz==1
describe, for example, the actions coveReq, and covered, that are && brake==1))} /*not satisfied */
implemented as two guarded commands. The first action models the
Listing 9: Flags of the generated code
message sent by the OBD component to the agent Coverage. The
second one models the message received by the OBD component The property p1 specifies that, always if the component OBD
from the agent Coverage. For example, as shown in Listing 7 in the sends the message covReq then it will receive a message covered or
implementation of coveReq, the guard part of the action specifies uncovered. This property is satisfied. The property p2 specifies that
that the buffer m 1 is full because there is a message to send, and the always if the OBD receives the message covered then it will receive
port pc2 (instantiation of the parameter p6 in Protocol) associated the message vmaz and the action emдcyBrake will be enabled. This
to the component Coverage is free. The command part of the action property is not satisfied, because there is the option of enabling the
specifies that the message will be sent in Pc2 and the buffer will be action ctrV elocity instead of emдcyBrake.
available.
proctype Protocol(port p1; ... ; port p7){
5 RELATED WORK
... In this paper, we propose compiling Reo circuits into Promela to for-
do mally verify the LTL properties of protocols of interactions among
::(full(m1) && full(p6.sync)) -> atomic{ m1?_m1; put(p6,_m1);} components. Formal verification of Reo specifications using a num-
/* covereq!*/
... ber of tools has already appeared in the literature (see below). Com-
:: (full(p3.data) && empty(m2)) -> atomic{take(p3,_p3);m2!_p3;} plementing this existing set of tools, in our work, we opted to use
/*covered*/ the SPIN model checker, because (i) it is one of the most advanced
ModComp 2018, Oct 2018, Danemark Benjamin Lion, Samir Chouali, and Farhad Arbab
analysis and verification tools available, and (ii) its Promela lan- a Promela program. We show the correctness of our translation,
guage resembles our guarded command formal specification of Reo which we have implemented as a back-end for the current Reo
circuits. We are not aware of a comprehensive work on verification compiler.
of Reo circuits using SPIN. We demonstrate the relevance of our work in a case study involv-
We proposed a formal framework for translation of Reo models ing design and verification of a railway component-based system.
into Promela. We use a transition-systems-based operational se- We use our compiler to translate the Reo specification of a protocol
mantics of Promela to express the formal semantics of Reo, through in this system into Promela, and use SPIN to verify LTL-specified
which we establish the correctness of our translation. Most of the properties, such as safety and liveness. In future work, we would
existing work uses constraint automata, instead, as operational like to support specification of LTL properties at design level as
semantics. an extension of constraint formula. This direction is justified by
Similar to our concerns, the CHARMY framework [20] also ad- the argument that in Reo, we can deduce the states of a protocol
dresses verifying LTL formulas expressing properties of component- entirely from the current state of its boundary ports and its internal
based systems. CHARMY is a UML based specification, where state memory. A designer, thus, has enough information at the level of
diagrams are counterparts of our agents, and sequence diagrams Reo to specify not just a protocol, but also its required LTL prop-
are that of our protocols. CHARMY defines a system as a set of erties, in some suitable constraint language, which our extended
state diagrams, coordinated by a sequence diagram. The CHARMY compilation can subsequently translate into Promela LTL statement
framework offers the possibility to translate its specification into on protocol states, for verification.
a Promela program, and thereby allows the verification of proper-
ties using SPIN. However, CHARMY allows composition of state REFERENCES
diagram specifications only, and not that of sequence diagrams. In [1] 2018. Link to the proofs. https://cloud.benjaminlion.fr/s/PtH6RtW056tuFJ4
our case, agents and protocol differ only in their implementations. [2] 2018. Reo github webpage. https://github.com/ReoLanguage/Reo
In Reo, protocols are constructed compositionally, and their com- [3] Farhad Arbab. 2004. Reo: A Channel-based Coordination Model for Component
position preserves and propagates synchrony. CHARMY does not Composition. Mathematical. Structures in Comp. Sci. 14, 3 (June 2004), 329–366.
https://doi.org/10.1017/S0960129504004153
seem to support such compositions.. Moreover, Reo can express [4] Farhad Arbab, Christel Baier, Frank de Boer, and Jan Rutten. 2007. Models and tem-
nesting of components, which is disallowed in CHARMY. Finally, poral logical specifications for timed component connectors. Software & Systems
properties of protocols are specified using property sequence chart Modeling 6, 1 (01 Mar 2007), 59–82. https://doi.org/10.1007/s10270-006-0009-9
(PSC) in CHARMY. In our approach, we require the specification of [5] Christel Baier, Tobias Blechmann, Joachim Klein, and Sascha Klüppelholz. 2009.
Formal Verification for Components and Connectors. In Formal Methods for
LTL properties directly in Promela, and leave as future work the Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, and Eric
integration of property specification at the design level. Madelaine (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 82–101.
Vereofy [5–7] is a model checking tool developed at the Uni- [6] Christel Baier, Tobias Blechmann, Joachim Klein, and Sascha Klüppelholz. 2009.
versity of Dresden to analyze and verify Reo connectors. Vere- A Uniform Framework for Modeling and Verifying Components and Connectors.
In Coordination Models and Languages, John Field and Vasco T. Vasconcelos (Eds.).
ofy has two input languages: the Reo Scripting Language (RSL), Springer Berlin Heidelberg, Berlin, Heidelberg, 247–267.
used to specify the coordination protocol, and a guarded command [7] Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, and Wolf-
language called Constraint Automata Reactive Module Language gang Leister. 2010. Design and Verification of Systems with Exogenous Coordi-
(CARML), a textual version of constraint automata used to specify nation Using Vereofy. In Leveraging Applications of Formal Methods, Verification,
and Validation, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin
the behavior of components. Vereofy allows the verification of tem- Heidelberg, Berlin, Heidelberg, 97–111.
poral properties expressed in LTL and CTL-like logics. In contrast [8] Christel Baier, Marjan Sirjani, Farhad Arbab, and Jan Rutten. 2006. Modeling
to Vereofy, in our work we use only one language, Promela, to component connectors in Reo by constraint automata. Science of Computer
specify both component behavior and coordination protocols. Programming 61, 2 (2006), 75 – 113. https://doi.org/10.1016/j.scico.2005.10.008
The constraint automata semantics for Reo was also considered Second International Workshop on Foundations of Coordination Languages and
Software Architectures (FOCLASA’03).
in [8] for defining and verifying bisimulation and language equiva- [9] Oscar Carrillo, Samir Chouali, and Hassan Mountassir. 2013. Incremental Mod-
lence between Reo connectors. In [3, 4], the authors considered time eling of System Architecture Satisfying SysML Functional Requirements. In
constraints, and proposed a timed version of constraint automaton Formal Aspects of Component Software - 10th International Symposium, FACS
to verify by model checking timed CTL properties. In [15, 16], the 2013, Nanchang, China, October 27-29, 2013, Revised Selected Papers. 79–99.
https://doi.org/10.1007/978-3-319-07602-7_7
authors use timed constraint automata and present a SAT-based [10] Dave Clarke, Jose Proenca, Alexander Lazovik, and Farhad Arbab. 2011. Channel-
approach for bounded model checking of real-time component con- based coordination via constraint satisfaction. Science of Computer Programming
nectors. Another verification approach based on SAT solvers was 76, 8 (2011), 681 – 710. https://doi.org/10.1016/j.scico.2010.05.004 Special issue on
proposed in [11], exploiting Alloy. This work allows analysis of Reo the 7th International Workshop on the Foundations of Coordination Languages
and Software Architectures (FOCLASA’08).
circuits and verification of their properties expressed as predicates [11] Kasper Dokter and Farhad Arbab. 2018. Rule-Based Form for Stream Con-
in the lightweight modeling language of Alloy, which is based on straints. In Coordination Models and Languages, Giovanna Di Marzo Serugendo
first-order relational logic. In [17, 18], Kokash et al. proposed a and Michele Loreti (Eds.). Springer International Publishing, Cham, 142–161.
framework for the verification of Reo circuits using the mCRL2 [12] Kasper Dokter and Farhad Arbab. 2018. Treo: Textual Syntax for Reo Connectors.
272 (06 2018), 121–135.
toolset (developed at the TU of Eindhoven). Their tool automati- [13] Gerard Holzmann. 2003. Spin Model Checker, the: Primer and Reference Manual
cally generates mCRL2 specifications from Reo graphical models. (first ed.). Addison-Wesley Professional.
The translation from Reo to mCRL2 uses the constraint automata [14] Sung-Shik T. Q. Jongmans and Farhad Arbab. 2012. Overview of Thirty Semantic
semantics of Reo. Formalisms for Reo. Sci. Ann. Comp. Sci. 22 (2012), 201–251.
[15] Stephanie Kemper. 2010. Compositional Construction of Real-Time Dataflow
Networks. In Coordination Models and Languages, Dave Clarke and Gul Agha
6 CONCLUSION AND FUTURE WORK (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 92–106.
In this paper, we presented sufficient conditions to compile a proto- [16] S. Kemper. 2012. SAT-based verification for timed component connectors. Science
col specified in Reo into a program implemented in Promela. We of Computer Programming 77, 7 (2012), 779 – 798. https://doi.org/10.1016/j.scico.
2011.02.003 (1) FOCLASA’09 (2) FSEN’09.
introduced the notions of ephemeral and permanent constraints; [17] Natallia Kokash, Christian Krause, and Erik de Vink. 2012. Reo + mCRL2 :
the former consist of constraints that change through time, reflect- A framework for model-checking dataflow in service compositions. Formal
ing the states of the environment or internal memories, whereas Aspects of Computing 24, 2 (01 Mar 2012), 187–216. https://doi.org/10.1007/
the latter consist of structural constraints that must hold invari- s00165-011-0191-6
[18] Natallia Kokash, Christian Krause, and Erik P. de Vink. 2010. Verification of
ably. We defined sufficient conditions for expressing the permanent Context-Dependent Channel-Based Service Models. In Formal Methods for Com-
constraint of a component in the guarded command form. We then ponents and Objects, Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede,
defined a translation of a formula in guarded command form to and Michael Leuschel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg,
Compiling Protocols to Promela and Verifying their LTL Properties ModComp 2018, Oct 2018, Danemark
21–40.
[19] Sebti Mouelhi, Khalid Agrou, Samir Chouali, and Hassan Mountassir. 2015. Object-
Oriented Component-Based Design using Behavioral Contracts: Application to
Railway Systems. In Proceedings of the 18th International ACM SIGSOFT Sympo-
sium on Component-Based Software Engineering, CBSE 2015, Montreal, QC, Canada,
May 4-8, 2015. 49–58. https://doi.org/10.1145/2737166.2737171
[20] P. Pelliccione, P. Inverardi, and H. Muccini. 2009. CHARMY: A Framework
for Designing and Verifying Architectural Specifications. IEEE Transactions on
Software Engineering 35, 3 (May 2009), 325–346. https://doi.org/10.1109/TSE.
2008.104
[21] Stavros Tripakis and Costas Courcoubetis. 1996. Extending promela and spin for
real time. In Tools and Algorithms for the Construction and Analysis of Systems,
Tiziana Margaria and Bernhard Steffen (Eds.). Springer Berlin Heidelberg, Berlin,
Heidelberg, 329–348.