Loïc Desgeorges
email: loic.desgeorges@univ-cotedazur.fr

Loïc Germerie Guizouarn

RSC to the ReSCu: Automated Verification of Systems of Communicating Automata ⋆

We present ReSCu, a model-checking tool for RSC (Realisable with Synchronous Communication) systems of communicating automata. Communicating automata are a formalism used to model communication protocols: each participant is represented by a finite state automaton, whose transitions are labelled by sending and receiving actions. In the general case, such automata exchanging messages asynchronously via FIFO or bag buffers are Turing-powerful, therefore most safety verification problems are undecidable. In RSC systems, the reception of a message may happen right after its send action. A lot of verification problems, e.g. reachability of a control state, are decidable for RSC systems. ReSCu checks whether a system is RSC, allowing to observe that a significant portion of protocols from the literature is RSC. This tool can also perform verification of safety properties for those systems, and is competitive in terms of time compared to non-RSC specific tools.

Introduction

Ensuring safety of communication protocols is admittedly a very important task. Systems of communicating automata (CA for short) are one of the formalisms modelling such protocols: each participant of the communication is represented by a finite state automaton, the transitions of which are labelled with actions, either to send or receive messages. Model-checking a system consists in verifying that it satisfies safety properties, e.g. whether an undesired configuration of control states is reachable. In this model, communications are asynchronous: messages are sent to unbounded buffers, waiting there to be received. The sender may immediately proceed with its subsequent actions. The main semantics for buffers are FIFO, for First In First Out, and bag. FIFO buffers behave like queues, messages are received in the same order as they were sent, whereas bag buffers allow receptions of messages in any order. Systems may be equipped with different structures of buffers named communication architecture. The most common ones being peer-to-peer, where there is one buffer per direction between each pair of participants, and mailbox, were each participant receives its messages from a single buffer.

From its asynchrony, comes a limitation of this model: buffers can encode the tape of a Turing Machine and therefore, deciding the reachability of a configuration of control states is undecidable [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. Different strategies arose to circumvent this difficulty, the main ones being using semi-algorithms for verification, and restricting systems to classes in which verification problems become decidable.

The latter approach is the one we used in [START_REF] Di Giusto | Towards Generalised Half-Duplex Systems[END_REF] and developed in [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF]. Intuitively, a system is Realisable with Synchronous Communication (RSC for short) if all its executions can be reorganised to mimic a synchronous behaviour, where send and receive actions of the same message happen at the same time. Reachability of a regular set of configurations was shown to be decidable for RSC systems. Membership to the class of RSC systems is decidable as well, allowing to select the protocols on which the reachability algorithms can be used.

We present ReSCu (for Realisable with Synchronous Communication), a model-checking tool for RSC systems of CA. This tool can answer whether a given system is RSC or not, and whether a specified bad configuration is reachable. ReSCu works on systems with any communication architecture (not restricted to peer-to-peer or mailbox) and either with bag or FIFO buffers.

Outline. After a discussion about related works, we will begin with some intuition about CA in Section 2. In Section 3, we present the tool itself, how it is implemented and how it can be used. Before concluding (Section 5), we will present some results and benchmarks we obtained with our tool in Section 4. [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF]. It takes a description of a system and a set of bad configurations (defined as QDDs [START_REF] Boigelot | Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract)[END_REF]), and checks whether a bad configuration is reachable. This tool implements various model-checking approaches, based on abstract interpretation. It is not limited to systems of a specific class. Contrary to ReSCu, most of these approaches are semi-algorithms and need a time-out to be set arbitrarily. However, the strength of McScM is the multiplicity of model-checking engines it provides, increasing the likelihood of a conclusive result for any system. We use its description language as a way to input systems in ReSCu.

Related works. The closest tool to ReSCu is McScM

The notion of stability, introduced in [START_REF] Basu | Automatic verification of interactions in asynchronous systems with unbounded buffers[END_REF], is close to RSC. A system is kstable if its behaviour with any bound k ′ > k is equivalent (with several notions of equivalence possible) to its behaviour with a bound k. Model-checking can be performed with bounded buffers for stable systems. Stability was shown to be undecidable for FIFO systems in [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF], but decidable with bag buffers (for a specific notion of equivalence) [START_REF] Akroun | Automated verification of automata communicating via FIFO and bag buffers[END_REF]. The authors of [START_REF] Akroun | Automated verification of automata communicating via FIFO and bag buffers[END_REF][START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF] developed STABC: a tool using semi-algorithms to check k-stability of systems. Contrary to ReSCu, it does not perform verification of safety properties, but provides only membership results.

Lange and Yoshida proposed another tool: KMC [START_REF] Lange | Verifying Asynchronous Interactions via Communicating Session Automata[END_REF], for k Multiparty Compatibility. It checks whether a system could have been obtained by projection of a global type, relying on the theory of Multiparty Session Types [START_REF] Honda | Multiparty asynchronous session types[END_REF] (another way to model distributed systems). If a system is k-MC, various safety properties are ensured, and it is not necessary to specify them as it is for McScM or ReSCu.

Communicating automata

We begin with a small example of protocol, borrowed from [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF].

Example 1 (Communication protocol). We will consider a generic client/server protocol, enhanced with a database logging activity. In this protocol, the client may send a request to the server, and when it receives a result for this request, it sends an acknowledgement back to the server. The server waits for a request, and upon receiving it, it sends a result to the client. After that, it waits for an acknowledgement from the client and sends a logging message to the database. Those behaviours can be repeated indefinitely.

⊓ ⊔

Figure 1 is a graphical representation of the system of CA modelling the protocol from Example 1. Each participant is represented by an automaton, which can change states by executing the actions labelling its transitions. An action i!v means that message v is sent in buffer i, and i?v that v is received from buffer i. In this system each participant receives all its messages in a single FIFO buffer (mailbox). Informally, a configuration is the product of the control states of each participant, paired with the content of the buffers. A configuration is reachable if a sequence of actions of the system can lead to it. We focus on safety properties that can be expressed as a regular language of 'bad' configurations of a system. We say that such a safety property is satisfied if no configuration of the language is reachable in the system.

Example 2 (Safety specifications). In Example 1, the configuration where the server is in state 1, and the client in state 0 is a bad configuration: it means those two participants are not at the same step of the protocol any more. Both the server and the client are not ready to receive the messages they are about to send each other. In this tiny example, it is easy to see that such a configuration is not reachable, but on bigger systems an automatic verification may be useful to ensure such properties. Another example: a set of bad configurations is formed by the ones where the server is in state 0, and the first message in buffer s is not req, preventing any further reception to happen for this participant (indeed, remember we use FIFO buffers, only the first message of a buffer may be received).

⊓ ⊔ Intuitively, a system of CA is RSC if send actions and their respective reception can happen at the same time: there is no need for another action to be performed between sending a message and receiving it. The work in [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF] provides formal definitions of CA and RSC systems, as well as algorithms for deciding membership to the class of RSC systems and reachability of a configuration. scm c l i e n t _ s e r v e r _ d a t a b a s e : nb_channels = 3; parameters : int req ; int res ; int log ; int ack ; automaton server : initial : 0 state 0: to 1: when true , 0 ? req ; state 1: to 2: when true , 1 ! res ; state 2: to 3: when true , 0 ? ack ; state 3: to 0: when true , 2 ! log ; automaton database : initial : 0 state 0: to 0: when true , 2 ? log ; automaton client : initial : 0 state 0: to 1: when true , 0 ! req ; state 1: to 2: when true , 1 ? res ; state 2: to 0: when true , 0 ! ack ;

ReSCu

ReSCu is a tool using the properties of RSC systems to perform model-checking.

It is an OCaml implementation of the algorithms in [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF]. While working on this implementation, we discovered a bug in the membership algorithm; we provide in Appendix A the fixed algorithms, generalised to take into account bag buffers. ReSCu provides a command line interface that takes a file describing a system of CA and its safety specifications, and outputs whether this system is RSC, and whether a bad configuration is reachable or not. If a bad configuration is reachable, ReSCu can display the execution leading to the safety counterexample.

Similarly, if non-RSC executions are possible, one of them may be displayed. This tool is available at [START_REF] Desgeorges | ReSCu archive[END_REF].

SCM description language. We chose, as an input format, the SCM language used in [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF]. This allowed to rely on the parser that was already available thanks to the developers of McScM, and to compare easily ReSCu with this tool. Figure 2 shows the SCM description of the system in Example 1. The set of messages is declared after the keyword parameters, and the number of buffers after the keyword nb channels ('channel' is the name used for buffers in SCM). An automaton is declared as a list of states, each of them containing a (possibly empty) list of transitions. SCM allows specification of model features we did not take into consideration, hence the 'when true' in the transitions, or the types of each message. Bad configurations are declared after the keyword 'bad states', each one of them being a list of control states and an optional regular expression describing buffer contents. The bad states of this listing correspond to the ones in Example 2.

Usage. The command line utility allows to check both membership and safety of a system: rescu -isrsc <system> checks whether the system described in the

Results

We used ReSCu on the set of examples provided with McScM, and we ported examples of systems available with STABC [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF] and KMC [START_REF] Lange | Verifying Asynchronous Interactions via Communicating Session Automata[END_REF]. This allowed to test our tool on a lot of systems, some of which modelling actual protocols.

Proportion of RSC systems in the wild. We used ReSCu to check the existence of RSC systems among examples from the literature. Using FIFO buffers, 30% of the systems from [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF], 60% of those from [START_REF] Lange | Verifying Asynchronous Interactions via Communicating Session Automata[END_REF] and 38% of those from [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF] are RSC. Using bag buffers, the results are respectively 12%, 41% and 11%. These figures are to be interpreted carefully however, as the examples coming from KMC and STABC are not all random examples. Examples of systems from KMC are CSA, for communicating session automata, which is a class of systems where there cannot be sending and receiving transitions leaving the same state. Some systems where even (slightly) modified to become CSA. To provide a more realistic overview of the importance of RSC systems in the literature, we show in Table 1 some membership results for interesting protocols that were featured in [START_REF] Lange | Verifying Asynchronous Interactions via Communicating Session Automata[END_REF] and [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF]. It shows a comparison of the results of ReSCu on one hand, and the results we reproduced with their respective tools on the other hand. The k value provided by STABC is a buffer bound that may be applied to the system without restricting its behaviour. As an example, we detail the results for a protocol: ring, a token passing protocol in a ring with four peers. The first algorithm, absint, did not provide a conclusive answer, and ran for about 19 seconds. The second one, armc, reached the time limit we set at 2 minutes without finishing. The next algorithms have four variants each, and even if cegar is the fastest in this example, one of its variant times out. Two of the variants of lart time out as well.

The protocol tcp error * is a simplified version of TCP, intentionally modified to be erroneous. It is not RSC, but we included it as ReSCu can still find one of its bad configurations. Even though ReSCu cannot certify that a non-RSC protocol is safe, it can still help finding bugs quickly.

The rightmost column in Tables 1a and1b gives an overview of the performance of the membership algorithm, compared to KMC and STABC respectively. Note that KMC checks the safety of a protocol, while knowing if a given system is RSC merely allows to know if our model-checking algorithm is suitable for it.

Conclusion

We presented ReSCu, a tool relying on the properties of RSC systems of communicating automata to verify safety of communication protocols. Through extensive testing and comparison with other tools, ReSCu proved to be performant, and allowed to notice that a significant portion of actual protocols from the literature are indeed RSC.

This tool has some limitations however: some systems are not RSC, and ReSCu cannot certify safety of those. Another drawback is that while other tools can check various safety properties taking only the description of the protocol, we need the users to define correctly the safety properties they want to check. While our current setting allows for some flexibility, generating bad configurations automatically for properties like unspecified reception, or progress (see [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF]), could be an interesting improvement of ReSCu, and is left as future work.

A Theoretical background

In this section, we present a condensed version of some theoretical of [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF]. We introduce two modifications: the first one is that we generalise our previous work to systems of CA with bag buffers, and the second one is that we fix a small bug that existed in the definition of A bv (defined in Section A.3).

A.1 Preliminaries

For a finite set S, S * denotes the set of finite words over S, w • w ′ denotes the concatenation of words w and w ′ , |w| denotes the length of word w, and ε denotes the empty word. We write L (A) for the language accepted by automaton A. For two sets S and I, we write b for an element of S I , and b i for the i-th component of b = (b i ) i∈I .

The set of all participants of a protocol is denoted P. For a participant p ∈ P, the communicating automaton A p is the tuple (L p , V p , I F p , I B p , Act p , δ p , l 0 p ) where: -L p is a finite set of control states, -V p is a finite set of messages, -I p = I F p ∪ I B p with I B p ∩ I F p = ∅ is a finite set of buffer identifiers where I B p (respectively I F p ) is the subset of bag (respectively FIFO) buffer identifiers, -Act p ⊆ I p × {! p , ? p } × V p is a finite set of actions, δ p ⊆ L p × Act p × L p is a finite set of transitions, and l 0 p is the initial control state. An action (denoted a) can be a send action: i! p v , meaning 'process p sends message v in buffer i', or a reception: i? p v meaning 'process p receives message v from buffer i'. To ease readability, the process is omitted when the context allows it. For a = i † v with † ∈ {!, ?}, buffer(a) = i.

A system, denoted by S, is a family of communicating automata, one per participant p ∈ P. For a system S = (A p ) p∈P :

-L S = p∈P L p is the set of global control states of the system: for l ∈ L S , l = (l p ) p∈P is a vector of control states, where for each participant p, l p is a control state of the automaton representing p; -V S = ∪ p∈P V p is the set of messages; -I S = I F S ∪ I B S is the set of buffer identifiers, where I F S = ∪ p∈P I F p is the set of FIFO buffers identifiers and I B S = ∪ p∈P I B p is the set of bag buffers identifiers; -Act S = ∪ p∈P Act p is the set of actions; δ S = (l, a, l ′ ) | ∃p ∈ P, (l p , a, l ′ p ) ∈ δ p , ∀q ̸ = p, l q = l ′ q . For an action a ∈ Act S , process(a) is the unique p ∈ P such that a ∈ Act p . A configuration (denoted γ) is a pair (l, b) where l is a global control states and b = (b i ) i∈I S is a vector of buffers, each b i being the concatenation of the messages contained in the buffer i. The initial configuration of a system is γ 0 = (l 0 , b 0 ), with l 0 = (l 0 p ) p∈P and b 0 = (ε) i∈I S . A transition of S is a tuple (γ, a, γ ′ ), often written γ and γ ′ = (l ′ , b ′ ) are two configurations, a is an action, and the following holds: Given an execution e = a 1 • . . . • a n , we say that {a j , a j ′ } ⊆ {a 1 , . . . , a n } with j < j ′ is a matching pair if there exist i, v, such that:

-(l, a, l ′ ) ∈ δ S -if a = i! p v , then b ′ i = v • b i , and for all j ∈ I S , j ̸ = i, b j = b ′ j -if a = i? p v , then for all j ∈ I S , j ̸ = i, b j = b ′ j and • if i ∈ I F S then b i = v • b ′ i • if i ∈ I B S then ∃w, w ′ ∈ V * S , b i = w • v • w ′ ,
-a j = i!v , -a j ′ = i?v , -and
• if i ∈ I F S then ∃k such that a j (respectively a j ′ ) is the k-th send action (respectively reception) on i in e,

• else ∃k such that a j (respectively a j ′ ) is the k-th send action (respectively reception) of message v on i in e.

For bag buffers, we say that when the same message is sent several times to a buffer, receptions of this message match the send actions in their order. A send action a j is unmatched in e if there is no j ′ such that {a j , a j ′ } is a matching pair. A communication (denoted c) is either a matching pair, or {a} with a an unmatched send. We say that two actions commute if they do not form a matching pair, and if they are not actions of the same type on a FIFO buffer. For an execution e = a 1 •. . .•a n , we say that a j ≺ e a j ′ , with {j, j ′ } ⊆ {1, . . . , n} if j < j ′ and a j does not commute with a j ′ . Intuitively, ≺ e represents causal dependencies between actions of an execution. Two executions e = a 1 • . . . • a n and e ′ = a ′ 1 • . . . • a ′ n are causally equivalent (denoted by e ∼ e ′ ) if there is a permutation σ of {1, . . . , n} such that:

for all i ∈ {1, . . . , n}, a ′ σ(i) = a i , and for all j, j ′ ∈ {1, . . . , n}, a j ≺ e a j ′ if and only if a ′ σ(j) ≺ e ′ a ′ σ(j ′ ) . A property P is a function from a system to a set of configurations. For a system S, P (S) is the set of configurations of S satisfying the property. A system is P safe if P (S) ∩ RS(S) = ∅. The idea behind P safety of a system is to describe the configurations that should not be reached, and to check whether all of them are indeed unreachable. We say that a property P is regular if, for all S, there exists a finite state automaton recognising a set of words that encodes configurations in P (S).

A.2 RSC systems

An execution is RSC if all its receptions are immediately preceded by the matching send action. Such an execution is a sequence of unmatched send actions and matching pairs. A system is RSC if all its executions are causally equivalent to an RSC execution.

The set of RSC executions of a system is regular. For a system S, we can compute an automaton A rsc (S) accepting all RSC executions feasible in S. Formally, for S a system, let

Σ S = {i!?v | i!v ∈ Act S , i?v ∈ Act S } ∪ {i!v | i!v ∈ Act S }
the set of all communications, where i!?v stands for the communication grouping the send and reception of v in buffer i. Let A rsc (S) = (L rsc , δ rsc , l 0 rsc , L f rsc ) be the non-deterministic finite state automaton over Σ S with L rsc = L S × 2 I F S its set of control states, l 0 rsc = (l 0 , ∅) its initial state, and L f rsc = L rsc its set of accepting states (all states are accepting). For c ∈ Σ S , (l, S) ∈ L rsc , (l ′ , S ′ ) ∈ L rsc , ((l, S) , c, (l ′ , S ′ )) ∈ δ rsc if:

-(l, b) c = ⇒ S (l ′ , b ′ ) for some b, b ′ such that for all i ∈ I F S , b i ̸ = ε iff i ∈ S, and b ′ i ̸ = ε iff i ∈ S ′ , and -if c = i!?v , i / ∈ S.

A.3 Membership

A bordeline violation is a minimal non-RSC execution. An execution e is a borderline violation if it is not causally equivalent to an RSC execution, and it is of the form e = e ′ • i?v with e ′ RSC. By [12, Lemma 9], a system S is RSC if and only if executions(S) contains no borderline violation. The set of borderline violations of a system is regular: we define now A bv , an automaton recognising all borderline violations of a system. Formally, for a system S, let Σ ? S = {i?v | i ∈ I S , v ∈ V S } the alphabet of all possible receptions of S, and A bv = L bv , δ bv , l 0 bv , ∅ , {l 1 bv } the nondeterministic finite state automaton over Σ S ∪ Σ ?

S such that

L bv = l 0 bv × 2 |I F S | , l 1 bv ∪ (I S × V S × Σ S × {0, 1}
), and for all c, c ′ ∈ Σ S , and for all i ∈ I S , v ∈ V S :

1. ((l 0 bv , S), i!?v , (l 0 bv , S)) ∈ δ bv if i / ∈ S 2. ((l 0 bv , S), i!v , (l 0 bv , S ′ )) ∈ δ bv if i ∈ I F S and S ′ = S ∪ {i}, or S = S ′ 3. ((l 0 bv , S), i!v , (i, v, i!v , 0) ∈ δ bv if i / ∈ S or i ∈ I B S 4. ((i, v, c, 0), c ′ , (i, v, c, 0)) ∈ δ bv if i ∈ I F S or c ′ ̸ = i!v 5. ((i, v, c, 0), c ′ , (i, v, c ′ , 1)) ∈ δ bv if either process(c ′ ) ∩ process(c) ̸ = ∅, or buffer(c) ∈ I F S and buffer(c) = buffer(c ′ ) 6. ((i, v, c, 1), c ′ , (i, v, c, 1)) ∈ δ bv if i ∈ I F S or c ′ ̸ = i!v 7. ((i, v, c, 1), c ′ , (i, v, c ′ , 1)) ∈ δ bv if either process(c ′ ) ∩ process(c) ̸ = ∅, or
buffer(c) ∈ I F S and buffer(c) = buffer(c ′ ) 8. ((i, v, c, 1), i?v , l 1 bv ) ∈ δ bv if process(c) = process(i?v ), or c is a matching pair and buffer(c) ∈ I F S and buffer(c) = i.

Theorem 1. Whether a system of communicating automata is RSC is decidable.

Proof. Let S be a system of communicating automata, and let L be the intersection of L (A bv (S)) on one hand, and L (A rsc (S)) • Σ ? S on the other hand, then L = ∅ iff S is RSC.

⊓ ⊔

A.4 Reachability

Regular properties describe a set of control states, and a content for the different buffers. The contents of the buffers are described as set of words, specifying an order for the messages. We opted for properties that do not describe the content of bag buffers, which are out of order. We encode configurations γ

= (l, b 1 , . . . , b |I S | ) with [γ] = l•#•b σ(1) •#•. . .•#•b σ(|I F S |) , with σ : |I F S | → |I S |
being a function defined such that σ(i) is the buffer index of the i-th FIFO buffer. This encoding is close to QDDs [START_REF] Boigelot | Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract)[END_REF].

For a regular property P , and a system S, let A(S) the automaton recognising the encoding of configurations S satisfying P . We will define an automaton A P (S) recognising executions leading to configurations satisfying P (configurations that are in P (S)). Intuitively, it works by recognising the content of each buffer independently. It does so by encoding in its states the state of A(S) corresponding to the accepting encoding of each buffer. A 'pebble' per buffer is placed non-deterministically on a state of A(S) and an unmatched send action i!v (contributing to the content of b i ) is accepted only if there is a transition accepting v from the state marked by the i-th pebble. Let A P (S) = L P (S) , δ P (S) , L 0 P (S) , F P (S) be a non-deterministic finite state automaton over the alphabet Σ S of communications where the set of control states is L P

(S) = L S × L S × L |I F S | A × L |I F S |
A , each control state (l S , l f , l A , l I ) corresponds to a situation where:

the current control state of S is l S , the target control state is l f , the i-th pebble is currently on state l A,i of A(S), -l I is a copy of the initial positions of the pebbles.

A state (l S , l f , l A , l I ) is initial if:

-l A = l I , -l A,1 ∈ δ * A(S) (l A,0 , l F • #), -l S = l 0 S .
A control state is accepting if:

-l S = l F , -for all i ∈ {1, . . . , |I F S | -1}, l A(S),i , #, l A(S),i+1 ∈ δ A(S) , and -l A,|I F S | ∈ F A(S) . Finally, a transition l S , l f , l A , l I , c, l ′ S , l ′ f , l ′ A , l ′ I ∈ δ P (S) if: -l F = l ′ F -l I = l ′ I -∃b, b ′ such that (l S , b) c = ⇒ S (l ′ S , b ′ ), -if c = i!v and i ∈ I F S , then l A,σ(i) , v, l ′ A,σ(i) ∈ δ A and for all j ∈ I F S , j ̸ = i, l A,σ(j) = l ′ A,σ(j) ; else, l A = l ′ A . Theorem 2.
Let S be an RSC system, and P a regular property, it is decidable whether S is P safe.

Proof. Let S be an RSC system, A rsc (S) recognises all RSC executions of S, and A P (S) recognises all executions of S leading to a configuration γ ∈ P (S); therefore L A rsc (S) ∩ A P (S) = ∅ iff S is P safe.

⊓ ⊔ Section 4.2 of [START_REF] Di Giusto | Multiparty half-duplex systems and synchronous communications[END_REF] provides a non exhaustive list of regular safety properties.

B Extended benchmark results

Tables 3 and4 show more results of membership testing. We can see that a majority the examples showcased in [START_REF] Lange | Verifying Asynchronous Interactions via Communicating Session Automata[END_REF] and [START_REF] Lakhdar Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF]

Figure 1 :

 1 Figure 1: Protocol from Example 1

Figure 2 :

 2 Figure 2: SCM representation of Example 1

  where γ = (l, b)

  and b ′ i = w • w ′ . An execution of a system S is a word on Act * S . We say that an execution e = a 1 • a 2 • . . . • a n is feasible in S if there exists a sequence of configurations γ 1 , γ 2 , . . . , γ n such that for all i ∈ {1, . . . , n}, γ i-and by abuse of notation we write a ∈ e if ∃i ∈ {1, . . . , n}, a = a i . The set of all feasible executions of S is denoted executions(S). A configuration γ of S is reachable if there exists an execution e ∈ Act * S such that γ 0 e = ⇒ S γ. The set of all reachable configurations of S is denoted RS(S).

Table 1 :

 1 Membership results of ReSCu compared with KMC and STABC. |P| is the number of participants, S the number of states, and T the number of transitions. trsc, t kmc and t stabc denote the time (in ms) of computation of ReSCu, KMC and STABC.

	Protocol	|P| S T RSC trsc k-MC tkmc	Protocol	|P| S T RSC trsc k	tstabc
	SMTP [16, 21]	2 64 108 Yes 17 Yes	34	Estelle specification [18]	2 7 9 No	5 max 82,625
	HTTP [17, 21]	2 12 48 Yes 17 Yes	28	FTP transfer [7]	3 20 17 Yes	6	4 89,465
	Elevator [6]	3 13 23 No	7 Yes	41	SQL server [22]	4 33 38 Yes 13	3 90,553
	Commit protocol [6] 4 12 12 Yes	4 Yes	15	SSH [20]	4 27 28 Yes	7	2 43,855
	Travel agency [21]	3 17 20 Yes	8 Yes	15	Bug report repository [13] 4 11 11 Yes	4 max 134,796
	SH [21]	3 22 30 Yes 18 Yes	33	Restaurant service [1]	3 16 16 No	5	2 52,793
	(a) Comparison with KMC		(b) Comparison with STABC, using FIFO buffers
					and 'strong equivalence'. max means the arbitrary
					limit for k, set at 10, was reached.

SCM file <system> is RSC, and rescu -mc <system> checks that no bad configuration is reachable. The two options can be combined in one call to ReSCu. Option -bag specifies that all buffers should be considered as bag buffers. In this case bad specifications including a description of the buffer contents are not accepted. For convenience while testing, we included a feature allowing to output a DOT representation of an SCM file. A video demonstrating the use of ReSCu is available at

[START_REF] Desgeorges | Demonstration video of ReSCu[END_REF]

.

Implementation choices.

McScM was designed as a framework, allowing addition of model-checking engines as modules. We opted for a stand-alone tool as the interface with McScM is way more involved than what is required for RSC algorithms. In addition, McScM is no longer maintained, and in its current state it is not possible to compile it with a modern version of OCaml.

  An extended version of those tables is available in Appendix B.Performance of our tool. We ran both our tool and McScM on several RSC examples from McScM, KMC and STABC, and compared the model-checking time. For the ported examples, we had to design some specifications, as the tools those systems came from focused only on membership to a class. The bad configurations we added are similar to the second one of Figure2: they enforce that, for a specific control state of a participant, no configuration where the first message of the buffer cannot be received is reached. For reference, we ran our testing on a laptop with an Intel Core i5-8250U CPU at 1.60GHz, equipped with 16Gb of RAM.

	Protocol	R eS C u	a b si n t	a rm c	ce g a r	la rt
	ring	137 (19,708) Tmax 382 1,928
	NonRegular 4	60	Tmax 13	10
	pop3	33	719 2,143 6,759 Tmax
	Nested	4	5	11 320 2045
	con disc reg 4	(21)	7	9	4
	tcp error * 4 (107)	26	66	10
	http-fsm	7	44	Tmax Tmax Tmax
	smtp	84	236	241 174 173
	FTP	51	29	54	61	82
	SSH	207 574	368 188 910
	Table 2: Model-checking time
	(in ms) of ReSCu and McScM.
	Figures in brackets correspond
	to inconclusive verification.

Table 2

 2 presents the times of computation of the different algorithms, averaged over 3 runs. The shortest time for each protocol is highlighted. The three horizontal sections of the table correspond to the origin of the examples: McScM, KMC and STABC, in that order. The runs that reached the time limit of 2 minutes are marked T max . The columns for cegar and lart present the best time of the four variants of these algorithms.

  is RSC.

	Protocol	|P| S T RSC trsc k-MC t kmc
	Client-Server-Logger [19] 3 11 12 No	3 Yes	17
	4 players game [36]	4 13 16 Yes 13 Yes	20
	Bargain [36]	3 9 8 Yes	4 Yes	35
	Filter collaboration [47]	2 6 10 Yes	4 Yes	33
	Alternating bit [35]	2 12 15 Yes	9 Yes	24
	TPMContract v2 [34]	2 10 14 Yes	4 Yes	31
	Sanitary agency [44]	4 25 30 Yes 15 Yes	39
	Logistic [40]	4 26 26 Yes	8 Yes	32
	Cloud system v4 [33]	4 14 16 Yes	6 Yes	22
	Commit protocol [6]	4 12 12 Yes	4 Yes	15
	Elevator [6]	3 13 23 No	7 Yes	41
	Dev system [42]	4 22 23 Yes	7 Yes	17
	Fibonacci [21]	2 6 6 Yes	3 Yes	17
	SH [21]	3 22 30 Yes 18 Yes	33
	Travel agency [21]	3 17 20 Yes	8 Yes	15
	SMTP [16, 21]	2 64 108 Yes 17 Yes	34
	HTTP [17]	2 12 48 Yes 17 Yes	28

Table 3 :

 3 Comparison between the membership results of ReSCu and KMC. |P| is the number of participants, S the number of states, and T the number of transitions. t rsc and t kmc are the time (in ms) of execution of ReSCu and KMC respectively.

	Protocol	|P| S T RSC trsc k	t stabc
	Estelle specification [18]	2 7 9 No	5 max 82,625
	News server [41]	2 10 10 No	5	3 54,507
	Client/Server [8]	2 6 10 Yes	4	1 26,130
	CFSM system [18]	2 6 7 No	4 max 81,911
	Promela program (1) [37] 2 6 6 No	4	2 39,905
	Promela program (2) [38] 2 6 7 Yes	4 max 81,555
	Web services [31]	3 13 12 Yes	5	2 53,084
	Trade system [30]	3 12 12 Yes	5	1 34,726
	FTP transfer [7]	3 20 17 Yes	6	4 89,465
	Client/Server [28]	3 15 15 Yes	5	2 53,040
	Mars explorer [24]	3 36 34 Yes	9	3 73,517
	Online computer sale [29] 3 26 26 Yes	8	2 53,112
	E-museum [27]	4 19 24 Yes	8	3 89,561
	Client/supplier [26]	3 31 33 Yes	9	2 53,094
	Restaurant service [1]	3 16 16 No	5	2 52,793
	Travel agency [46]	3 34 38 Yes 10	4 102,494
	Vending machine [32]	3 15 14 Yes	5	2 53,062
	Travel agency [23]	3 43 56 No 13	3 71,339
	Train station [45]	4 20 18 Yes	8	2 66,030
	Factory job manager [25] 4 20 20 Yes	7	2 65,774
	Bug report repository [13] 4 11 11 Yes	4 max 134,796
	Cloud application [33]	4 8 10 No	6 max 134,655
	Sanitary agency [43]	4 35 42 Yes 30	3 88,927
	SQL server [22]	4 33 38 Yes 13	3 90,553
	SSH [20]	4 27 28 Yes	7	2 43,855
	Booking system [39]	5 45 50 Yes 48	2 78,625

Table 4 :

 4 Comparison between the membership results of ReSCu and STABC, using FIFO buffers and 'strong equivalence'. |P| is the number of participants, S the number of states, and T the number of transitions. max means the arbitrary limit for k, set at 10, was reached. t rsc and t stabc are the time (in ms) of execution of ReSCu and STABC respectively.

⋆ This work has been supported by the French government, through the EUR DS4HInvestments in the Future project managed by the National Research Agency (ANR) with the reference number ANR-17-EURE-0004.

Acknowledgements. We would like to thank all the COORDINATION reviewers for their comments that greatly improved the present paper.