<figure><img src="image_1.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# RSC to the ReSCu: Automated Verification of Systems of Communicating Automata*

Loïc Desgeorges and Loïc Germerie Guizouarn

Université Côte d'Azur, CNRS, I3S, Sophia Antipolis, France
{loic.desgeorges,loic.germerie-guizouarn}@univ-cotedazur.fr

**Abstract** We present ReSCu, a model-checking tool for RSC (Realizable 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.

## 1 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.

<footnote>* This work has been supported by the French government, through the EUR DS4H Investments in the Future project managed by the National Research Agency (ANR) with the reference number ANR-17-EURE-0004.</footnote>
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 configura-
tion of control states is undecidable [8]. 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 [13] and developed in [12]. Intuit-
ively, 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. Reach-
ability 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 reach-
able. ReSCu works on systems with any communication architecture (not re-
stricted 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 in-
tuition 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.

***Related works.*** The closest tool to ReSCu is McScM [15]. It takes a descrip-
tion of a system and a set of bad configurations (defined as QDDs [5]), 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.

The notion of *stability*, introduced in [4], is close to RSC. A system is *k*-stable 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 [3], but decidable with bag buffers (for a specific notion of equivalence) [2]. The authors of [2, 3] 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 [20], for *k* Multiparty Com-
patibility. It checks whether a system could have been obtained by projection of
a global type, relying on the theory of Multiparty Session Types [16] (another
way to model distributed systems). If a system is *k*-MC, various safety proper-
ties are ensured, and it is not necessary to specify them as it is for McScM or
ReSCu.
<figure><img src="image_2.png" /><figcaption>Figure 1: Protocol from Example 1</figcaption></figure>

## 2 Communicating automata

We begin with a small example of protocol, borrowed from [3].

*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 [12] 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.
<table><thead><tr><th>Protocol</th><th>|P|</th><th>S</th><th>T</th><th>RSC</th><th>t<sub>rsc</sub></th><th>k-MC</th><th>t<sub>kmc</sub></th></tr></thead><tbody><tr><td>SMTP [17, 22]</td><td>2</td><td>64</td><td>108</td><td>Yes</td><td>17</td><td>Yes</td><td>34</td></tr><tr><td>HTTP [18, 22]</td><td>2</td><td>12</td><td>48</td><td>Yes</td><td>17</td><td>Yes</td><td>28</td></tr><tr><td>Elevator [6]</td><td>3</td><td>13</td><td>23</td><td>No</td><td>7</td><td>Yes</td><td>41</td></tr><tr><td>Commit protocol [6]</td><td>4</td><td>12</td><td>12</td><td>Yes</td><td>4</td><td>Yes</td><td>15</td></tr><tr><td>Travel agency [22]</td><td>3</td><td>17</td><td>20</td><td>Yes</td><td>8</td><td>Yes</td><td>15</td></tr><tr><td>SH [22]</td><td>3</td><td>22</td><td>30</td><td>Yes</td><td>18</td><td>Yes</td><td>33</td></tr></tbody></table>

(a) Comparison with KMC

<table><thead><tr><th>Protocol</th><th>|P|</th><th>S</th><th>T</th><th>RSC</th><th>t<sub>rsc</sub></th><th>k</th><th>t<sub>stabc</sub></th></tr></thead><tbody><tr><td>Estelle specification [19]</td><td>2</td><td>7</td><td>9</td><td>No</td><td>5</td><td>max</td><td>82,625</td></tr><tr><td>FTP transfer [7]</td><td>3</td><td>20</td><td>17</td><td>Yes</td><td>6</td><td>4</td><td>89,465</td></tr><tr><td>SQL server [23]</td><td>4</td><td>33</td><td>38</td><td>Yes</td><td>13</td><td>3</td><td>90,553</td></tr><tr><td>SSH [21]</td><td>4</td><td>27</td><td>28</td><td>Yes</td><td>7</td><td>2</td><td>43,855</td></tr><tr><td>Bug report repository [14]</td><td>4</td><td>11</td><td>11</td><td>Yes</td><td>4</td><td>max</td><td>134,796</td></tr><tr><td>Restaurant service [1]</td><td>3</td><td>16</td><td>16</td><td>No</td><td>5</td><td>2</td><td>52,793</td></tr></tbody></table>

(b) Comparison with STABC, using FIFO buffers and 'strong equivalence'. max means the arbitrary limit for k, set at 10, was reached.

<caption>Table 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. t<sub>rsc</sub>, t<sub>kmc</sub> and t<sub>stabc</sub> denote the time (in ms) of computation of ReSCu, KMC and STABC.</caption>

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 [9].

*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.

# 4 Results

We used ReSCu on the set of examples provided with McScM, and we ported examples of systems available with STABC [3] and KMC [20]. 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 [15], 60% of those from [20] and 38% of those from [3] 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 [20] and [3]. 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. An extended version of those tables is available in [11].

*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 Figure 2: 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.

<table><caption>Table 2: Model-checking time (in ms) of ReSCu and McScM. Figures in brackets correspond to inconclusive verification.</caption><thead><tr><th>Protocol</th><th>ReSCu</th><th>absint</th><th>armc</th><th>cegar</th><th>lart</th></tr></thead><tbody><tr><td>ring</td><td>137</td><td>(19,708)</td><td>T<sub>max</sub></td><td>382</td><td>1,928</td></tr><tr><td>NonRegular</td><td>4</td><td>60</td><td>T<sub>max</sub></td><td>13</td><td>10</td></tr><tr><td>pop3</td><td>33</td><td>719</td><td>2,143</td><td>6,759</td><td>T<sub>max</sub></td></tr><tr><td>Nested</td><td>4</td><td>5</td><td>11</td><td>320</td><td>2045</td></tr><tr><td>con.disc.reg</td><td>4</td><td>(21)</td><td>7</td><td>9</td><td>4</td></tr><tr><td>tcp.error*</td><td>4</td><td>(107)</td><td>26</td><td>66</td><td>10</td></tr><tr><td>http-fsm</td><td>7</td><td>44</td><td>T<sub>max</sub></td><td>T<sub>max</sub></td><td>T<sub>max</sub></td></tr><tr><td>smtp</td><td>84</td><td>236</td><td>241</td><td>174</td><td>173</td></tr><tr><td>FTP</td><td>51</td><td>29</td><td>54</td><td>61</td><td>82</td></tr><tr><td>SSH</td><td>207</td><td>574</td><td>368</td><td>188</td><td>910</td></tr></tbody></table>

Table 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.

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 and 1b 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.

# 5 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 [12]), could be an interesting improvement of ReSCu, and is left as future work.

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

## Data Availability Statement

The artifact is available in the Software Heritage repository:

swh:1:dir:a9fb15adfc33656029d9d84d34ec34c129ebfc34

## References

[1] Wil M. P. van der Aalst, Arjan J Mooij, Christian Stahl and Karsten Wolf. ‘Service interaction: Patterns, formalization, and analysis’. In: *Formal Methods for Web Services, SFM, Advanced Lectures 9* (2009). Publisher: Springer, pp. 42–88.

[2] Lakhdar Akroun and Gwen Salaün. ‘Automated verification of automata communicating via FIFO and bag buffers’. In: *Formal Methods Syst. Des. 52.3* (2018), pp. 260–276. DOI: 10.1007/s10703-017-0285-8.

[3] Lakhdar Akroun, Gwen Salaün and Lina Ye. ‘Automated Analysis of Asyn- chronously Communicating Systems’. In: *Model Checking Software - 23rd International Symposium, SPIN, Proceedings*. Vol. 9641. Lecture Notes in Computer Science. Springer, 2016, pp. 1–18. DOI: 10.1007/978-3-319- 32582-8_1.

[4] Samik Basu and Tevfik Bultan. ‘Automatic verification of interactions in asynchronous systems with unbounded buffers’. In: *ACM/IEEE International Conference on Automated Software Engineering, ASE*. ACM, 2014, pp. 743–754. DOI: 10.1145/2642937.2643016.

[5] Bernard Boigelot and Patrice Godefroid. ‘Symbolic Verification of Com- munication Protocols with Infinite State Spaces Using QDDs (Extended Abstract)’. In: *Computer Aided Verification, 8th International Conference, CAV, Proceedings*. Vol. 1102. Lecture Notes in Computer Science. Springer, 1996, pp. 1–12. DOI: 10.1007/3-540-61474-5_53.
[6] Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer. 'On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony'. In: Computer Aided Verification - 30th International Conference, CAV, Held as Part of the Federated Logic Conference, FloC, Proceedings, Part II. Vol. 10982. Lecture Notes in Computer Science. Springer, 2018, pp. 372-391. doi: 10.1007/978-3-319-96142-2_23.

[7] Andrea Bracciali, Antonio Brogi and Carlos Canal. 'A formal approach to component adaptation'. In: Journal of Systems and Software 74.1 (2005). Publisher: Elsevier, pp. 45-54.

[8] Daniel Brand and Pitro Zafipropulo. 'On Communicating Finite-State Machines'. In: Journal of the ACM 30.2 (1983), pp. 323-342. doi: 10.1145/322374.322380.

[9] Loïc Desgeorges and Loïc Germerie Guizouarn. Demonstration video of ReSCu. https://seafile.celazur.fr/f/bfa8e1380ce540f5bddb/?dl=1.

[10] Loïc Desgeorges and Loïc Germerie Guizouarn. ReSCu archive. https://archive.softwareheritage.org/browse/origin/directory/?origin_url=https://src.koda.cnrs.fr/loic.germerie.guizouarn/rescu.

[11] Loïc Desgeorges and Loïc Germerie Guizouarn. RSC to the ReSCu: Automated Verification of Systems of Communicating Automata. https://hal.scienceshal-04090204.

[12] Cinzia Di Giusto, Loïc Germerie Guizouarn and Etienne Lozes. 'Multi-party half-duplex systems and synchronous communications'. In: Journal of Logical and Algebraic Methods in Programming 131 (2023), p. 100843. ISSN: 2352-2208. doi: 10.1016/j.jlamp.2022.100843.

[13] Cinzia Di Giusto, Loïc Germerie Guizouarn and Étienne Lozes. 'Towards Generalised Half-Duplex Systems'. In: 14th Interaction and Concurrency Experience, ICE, Proceedings. Vol. 347. EPTCS. 2021, pp. 22-37. doi: 10.4204/EPTCS.347.2.

[14] Gregor Gößler and Gwen Salaün. 'Realizability of Choreographies for Services Interacting Asynchronously'. In: Formal Aspects of Component Software - 8th International Symposium, FACS, Revised Selected Papers. Vol. 7253. Lecture Notes in Computer Science. Springer, 2011, pp. 151-167. doi: 10.1007/978-3-642-35743-5_10.

[15] Alexander Heußner, Tristan Le Gall and Grégoire Sutre. 'McScM: A General Framework for the Verification of Communicating Machines'. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings. Vol. 7214. Lecture Notes in Computer Science. Springer, 2012, pp. 478-484. doi: 10.1007/978-3-642-28756-5_34.

[16] Kohei Honda, Nobuko Yoshida and Marco Carbone. 'Multiparty asynchronous session types'. In: 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Proceedings. ACM, 2008, pp. 273-284. doi: 10.1145/1328438.1328472.
[17] Raymond Hu. 'Distributed programming using Java APIs generated from session types'. In: *Behavioural Types: from Theory to Tools* (2017). Publisher: River Publishers, pp. 287–308.

[18] Raymond Hu and Nobuko Yoshida. 'Hybrid session verification through endpoint API generation'. In: *Fundamental Approaches to Software Engineering, FASE, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings 19*. Springer, 2016, pp. 401–418.

[19] Thierry Jéron and Claude Jard. 'Testing for unboundedness of fifo channels'. In: *Theoretical Computer Science* 113.1 (1993). Publisher: Elsevier, pp. 93–117.

[20] Julien Lange and Nobuko Yoshida. 'Verifying Asynchronous Interactions via Communicating Session Automata'. In: *Computer Aided Verification - 31st International Conference, CAV, Proceedings, Part I*. Vol. 11561. Lecture Notes in Computer Science. Springer, 2019, pp. 97–117. DOI: 10.1007/978-3-030-25540-4_6.

[21] José Antonio Martín and Ernesto Pimentel. 'Contracts for security adaptation'. In: *The Journal of Logic and Algebraic Programming* 80.3 (2011). Publisher: Elsevier, pp. 154–179.

[22] Rumyana Neykova, Raymond Hu, Nobuko Yoshida and Fahd Abdeljallal. 'A session type provider: compile-time API generation of distributed protocols with refinements in F#'. In: *27th International Conference on Compiler Construction, CC, Proceedings*. ACM, 2018, pp. 128–138. DOI: 10.1145/3178372.3179495.

[23] Pascal Poizat and Gwen Salaün. 'Adaptation of open component-based systems'. In: *Formal Methods for Open Object-Based Distributed Systems: 9th IFIP WG 6.1 International Conference, FMOODS, Proceedings 9*. Springer, 2007, pp. 141–156.