Ocan Sankur

Jean-Pierre Talpin

An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP

We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization protocols. We develop abstraction techniques for parameterized model checking of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation protocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter.

Introduction

One of the apparently simplest services in any loosely-coupled distributed system is the time service. Usually, a client in such a system, e.g. your laptop, simply posts an NTP (network time protocol) request to any registered server and uses the first reply. In many such systems, however, the accuracy and reliability of the time service are critical: clients of traffic and power grids, banking and transaction networks, automated factories and supply plants, acutely depend on a reliable and accurate measure of time.

To make things worse, most cyber-physical system in such distributed networks rely on a quasi-synchronous hypothesis that critically relies on drift and jitter bounds provided by time synchronisation protocols. In a remedy for this Achille's heel of the "Internet of things", fault-tolerant and self-calibrating protocols have been proposed, such as the open source flooding time synchronisation protocol (FTSP) of Tiny OS, Google's True Time API, as well as commercial solutions, such as IGS' Real-Time Service. It is critical to provide such services to the 21st Century's Internet as is it to provide proof of their correctness.

Our goal is to develop both modular and scalable verification techniques for time synchronisation protocols. Towards this aim, in this paper, we concentrate on leader election protocols which are at the basis of several time synchronisation protocols where the nodes in the network synchronise their clocks to that of the elected leader. Leader election protocols pose exciting benchmarks and case studies to the verification of distributed systems design. These have been the subject of formal proofs or model-checking, e.g. Chang-Robert's algorithm [START_REF] Chang | An improved algorithm for decentralized extremafinding in circular configurations of processes[END_REF][START_REF] Garavel | Specification and verification of various distributed leader election algorithms for unidirectional ring networks[END_REF], and that of Dolev-Klaweh-Rodeh [START_REF] Dolev | An o (n log n) unidirectional distributed algorithm for extrema finding in a circle[END_REF][START_REF] Fredlund | Formal verification of a leader election protocol in process algebra[END_REF].

The root election part of FTSP [START_REF] Maróti | The flooding time synchronization protocol[END_REF], available in open-source in the implementation of Tiny OS, has drawn attention from the formal verification community. Kusy and Abdelwahed [START_REF] Kusy | Ftsp protocol verification using spin[END_REF] model-check FTSP root election using SPIN, showing that a 4-node FTSP network is guaranteed to converge to a single root node. McInnes [START_REF] Mcinnes | Model-checking the flooding time synchronization protocol[END_REF] verifies root-convergence for 7-node models using the FDR2 model checker, and also considers time-convergence properties, i.e. whether all nodes agree on the time of the root node. Tan et al. [START_REF] Tan | Analyzing the robustness of ftsp with timed automata[END_REF] use timed automata to introduce a more realistic simulation model of wireless sensor networks (WSN) with transmission delays and node failures and check the FTSP against these. They identify an error in a scenario where two root nodes fail continuously.

Parameterized Verification

The major issue when model checking such distributed protocols is the state explosion problem due to the large number of nodes in the protocol. Several works have concentrated on given network topologies, for instance, a grid of fixed size, e.g. [START_REF] Mcinnes | Model-checking the flooding time synchronization protocol[END_REF]. To model check properties for an arbitrary number of nodes, parameterized verification techniques have been considered. Although the general problem is undecidable [START_REF] Apt | Limits for automatic verification of finite-state concurrent systems[END_REF], decidability has been shown in several cases, by proving cutoffs [START_REF] Emerson | Reasoning about rings[END_REF] either on fully connected topologies or particular ones such as rings. Compositional model checking techniques were used in [START_REF] Mcmillan | Correct Hardware Design and Verification Methods[END_REF] for model checking a cache coherence protocol.

Contributions

We present an abstraction technique for the parameterized verification of distributed protocols with unique identifiers and apply it for model checking the leader election part of the FTSP. Our model for FTSP is more precise compared to the previous works in several aspects. In fact, we consider asynchronous communication between nodes rather than instantaneous broadcasts, and we model the periodically executed tasks as run with local clocks that are subject to imperfections. We were able to model check that a unique leader is elected starting at an arbitrary configuration, assuming no fault occurs during this period. This corresponds to checking fault recovery, that is, proving the protocol correct following an arbitrary fault. Thus, if we prove that the leader is elected within N steps in this setting, then following any fault, a unique leader is elected again within N steps in the worst case.

Our parameterized verification algorithm allows us to check FTSP a) for arbitrary topologies in which the maximal distance to the future leader is at most K, b) where each node evolves under clock deviations whose magnitude can be adjusted, c) where communication between nodes are either synchronous or asynchronous. As an example, we were able to model check the protocol for K = 7 in the synchronous case, and for K = 5 in the asynchronous case. Graphs with K = 7 include 2D grids with 169 nodes (or 3D grids with 2197 nodes), where the future leader is at the middle. For K = 5, these include 2D grids with 81 nodes (and 729 in 3D). Observe that grids of size 60 were considered for simulation in [START_REF] Maróti | The flooding time synchronization protocol[END_REF], which is out of the reach of previous model checking attempts.

We believe our parameterized verification technique can be adapted to other distributed protocols that work in a similar fashion, e.g. [START_REF] Vasudevan | Design and analysis of a leader election algorithm for mobile ad hoc networks[END_REF]. Our project is to extend our technique by integrating non-functional characteristics that have an impact on the accuracy and reliability of these protocols: electronic hazards (inaccuracy in physical clocks fabric), environmental hazards (temperature of clients environment), power hazards (capacity and stability of clients power source). Protocols accounting for such cyber-physical characteristics are being developed in the NSF Roseline and our goal is to prove their correctness.

More on Related Work Our parameterized verification approach is inspired by [START_REF] Chou | A simple method for parameterized verification of cache coherence protocols[END_REF] where an abstraction technique is given for parameterized model checking against safety properties in cache coherence protocols. Using the fact that such systems are symmetric, the main idea is to isolate a pair of nodes and abstract away other nodes as an abstract environment. In our work, the systems we consider are not symmetric since the nodes have unique identifiers which influence their behaviors and the network topology is arbitrary. We thus deal with these issues in order to lift the technique in our case. Another work introduces a refinement of existential abstraction for parameterized model checking: in [START_REF] Clarke | Proving ptolemy right: The environment abstraction framework for model checking concurrent systems[END_REF], an abstraction is obtained by isolating a component, and abstracting away the other nodes by summarizing which control states are occupied by some component, which is similar to counter abstraction [START_REF] Pnueli | Computer Aided Verification: 14th International Conference, CAV 2002[END_REF]. Parameterized verification techniques have been studied for fault-tolerant distributed systems with Byzantine or other types of failures [START_REF] John | Parameterized model checking of fault-tolerant distributed algorithms by abstraction[END_REF]. Such protocols often consider threshold guards, which are used to make sure that a given number of messages have been received from different processes. The authors define abstractions on the set of participating nodes with predicates that use these thresholds. This approach is not applicable in our case due to our network topologies, and that the nodes do not use such thresholds. Parameterized verification results on processes with unique identifiers are more rare but decidability was obtained under some restrictions [START_REF] Delzanno | Reachability Problems: 7th International Workshop[END_REF].

Overview of the Abstraction Technique

Let us give an overview of our parameterized verification technique. Let us call future leader the node that is expected to become the leader. We consider classes of graphs G K in which the maximal distance from the future leader is K. We show how to verify the protocol for all network topologies in G K , for given K, essentially in two steps:

1. We apply abstractions on local variables including node identifiers, which reduce the state spaces and renders all nodes anonymous except for the future leader. In fact, the variables storing node ids are mapped to a Boolean domain; encoding whether the node id is that of the future leader or not. 2. We then pick a shortest path of length K from the future leader. We derive an abstract model where all nodes that appear on this path are kept as concrete, but all other nodes have been abstracted away.

For each K, we thus construct a model A(K) and prove that it is an overapproximation of the protocol on all topologies in G K . We make sure that A(K) does not depend on the choice of the shortest path; if the property holds on A(K), it holds on the whole network. The approach is illustrated in Fig. 1.

Clock Deviations

We are interested in protocols where each node executes a periodic action with identical period. However, this period is subject to small deviations due to environment and hardware differences. Rather than using real-time verification techniques [START_REF] Alur | A theory of timed automata[END_REF], we use a recent and simple way of modeling behaviors under such conditions. In [START_REF] Desai | Approximate synchrony: An abstraction for distributed almost-synchronous systems[END_REF], it is shown that an approximately synchronous semantics, where one bounds the progress of each process with respect to that of (a) A network with a grid topology. The future root, that is, the node with the smallest ID is shown with a white dot.

(b) We choose a path from the future root to some node (c) We model all nodes on the path concretely, and summarize the behavior of all other nodes by one abstract node Fig. 1: Shortest-path abstraction illustrated on a grid topology with K = 3. others, over-approximates the behaviors under bounded clock deviations, which makes it possible to use finite-state model checking techniques and tools.

Incremental Verification We use an incremental proof technique for model checking A(K) for increasing values of K, as follows. To check A(K +1), we first model check A(K), proving that all nodes eventually agree on the leader. Our abstraction method implies that the first K components in A(K +1) eventually agree on the leader since their part of the graph belongs to G K Thus, to check A(K + 1), we initialize the first K nodes at states where they have agreed on the future leader. This significantly simplifies the verification process.

Overview Section 2 presents definitions for the formalization of our approach. We describe FTSP in detail in Section 3, as well as the abstraction steps explained above, and the incremental verification result. A semi-algorithm for model checking and experimental results on FTSP are presented in Section 4.

Definitions

Communicating Processes A process is an automaton A = (S, s init , δ, Σ) where S are states, s init ⊆ S are the initial states, and δ ⊆ S × Σ × S a transition relation, with alphabet Σ. A transition (s, a, s ) ∈ δ is also written δ(s, a, s ) or s a -→ s , and we write s a -→ to mean that there is no s such that δ(s, a, s ). We consider predicates that are evaluated on the states of a given process. Let P be a finite number of predicates where each p ∈ P is a subset p ⊆ S, representing states in which the predicate is satisfied. We write s |= p if s ∈ p.

We define simulation between two processes as follows. Consider process A = (S, s init , δ, Σ) with predicates P and A = (S , s init , δ , Σ ) with predicates P , an alphabet Σ ⊆ Σ, and any function α : Σ → Σ . Assume that P and P are in bijection denoted by p → p for each p ∈ P. We say that A (Σ , α)-simulates A, written A Σ ,α A if there exists R ⊆ S × S such that s init × s init ⊆ R and ∀(s, s ) ∈ R, ∀a ∈ Σ , t ∈ S, δ(s, a, t) ⇒ ∃t ∈ S , δ (s , α(a), t ) ∧ (t, t ) ∈ R, and moreover for all (s, s ) ∈ R and p ∈ P, s |= p ⇔ s |= p . When α is the identity and Σ = Σ, this is the usual simulation notion, and we write Σ . Given a process A, let us define the mapping of A by α the process obtained by A by replacing the transitions δ by δ = {(s, α(a), s ) | (s, a, s ) ∈ δ}. It is clear that the mapping A (Σ, α)-simulates A.

For any positive integer N , we write

A N Σ ,α A if there exist R 1 , . . . , R N ⊆ S × S such that s init × s init ⊆ R 1 and for all 1 ≤ i ≤ N -1, ∀(s, s ) ∈ R i , ∀a ∈ Σ , t ∈ S, δ(s, a, t) ⇒ ∃t ∈ S , δ (s , α(a), t ) ∧ (t, t ) ∈ R i+1 ; and for all (s, s ) ∈ R 1 ∪ . . . ∪ R n , s |= p ⇔ s |= p . The latter relation is called simulation up to N .
We define a particular alphabet Σ to model synchronization by rendez-vous. Let us fix n > 0, and define the set of identifiers Id = {1, . . . , n}. Consider also an arbitrary set Msg of message contents. We denote [1, n] = {1, . . . , n}. We define the alphabet

Σ(Id, Msg) = {i!(j, m) | i ∈ Id, j ∈ Id, m ∈ Msg} ∪ {j?(i, m) | i, j ∈ Id, m ∈ Msg} ∪ {τ }.
We let Σ = Σ(Id, Msg). We will later use different sets Id and Msg to define alphabets. Intuitively, the label i!(j, m) means that a process with id i sends message m to process with id j, while j?(i, m) means that process j receives a message m from process i. The special symbol τ is an internal action. For a subset

I ⊆ Id, let Σ I (Id, Msg) = {τ } ∪ {i!(j, m), i?(j, m) ∈ Σ(Id, Msg) | i ∈ I, j ∈ Id, m ∈ Msg}.
These are the actions where the senders and receivers have ids in

I. A τ -path of A is a sequence s 1 s 2 . . . of states such that for all i ≥ 1, δ(s i , τ, s i+1 ). An initialized τ -path is such that s 1 ∈ s init .
Graphs To formalize network topologies, we consider undirected graphs. A graph is a pair G = (V, E) with V = {1, . . . , n} and E ⊆ V × V which is symmetric. Let G(n) the set of graphs on vertex set {1, . . . , n}. In our setting, a node will be identified with a process id. For a graph G = (V, E), and node i, let N G (i) = {j ∈ V, (i, j) ∈ E}, the neighborhood of i. We define the following subclass of graphs. For any positive number K ≥ 0, let G K (n) denote the set of graphs of G(n) in which the longest distance between node 1 and any other node is at most K. Here, distance is the length of the shortest path between two nodes. Asynchronous Product We now define the product of two processes A and A following CCS-like synchronization [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. Intuitively, processes synchronize on send i!(j, m) and receive j?(i, m), and the joint transition becomes a τ -transition. Definition 1. Consider A = (S, s init , δ, Σ J (Id, Msg)) and A = (S , s init , δ , Σ J (Id, Msg)) where J, J ⊆ {1, . . . , n} with J

∩ J = ∅. Let G = (V, E) ∈ G(n).
We define the product A = A G A as (S , s init , δ , Σ J∪J ) where S = S × S , s init = s init ×s init , and δ is defined as follows. There are four types of transitions.

Internal transitions are defined by (s 1 , s 1 )

τ -→ (s 2 , s 2 ) whenever δ(s 1 , τ, s 2 ) ∧ s 1 = s 2 or δ (s 1 , τ, s 2 ) ∧ s 1 = s 2 .
Synchronizing transitions are defined as

(s 1 , s 1 ) τ -→ (s 2 , s 2 ) whenever ∃i ∈ J, j ∈ J , m ∈ Msg with i ∈ N G (j), s.t. either s 1 i!(j,m) ----→ s 2 and, s 1 j?(i,m) -----→ s 2 ; or, s 1 j!(i,m) ----→ s 2 , and s 1 i?(j,m) ----→ s 2 .
Sending transitions without matching receive is defined as

(s 1 , s 1 ) i!(j,m) ----→ (s 2 , s 2 ) whenever i ∈ J, j ∈ J , m ∈ Msg, i ∈ N G (j) s.t. either s 1 i!(j,m) ----→ s 2 , s 1 = s 2 ; or, i ∈ J , j ∈ J, s 1 i!(j,m) ----→ s 2 , s 1 = s 2 .
Receive transitions without matching send are defined, for all i, j ∈ Id and

m ∈ Msg, (s 1 , s 1 ) i?(j,m) ----→ (s 2 , s 2 ) whenever i ∈ N G (j) and either i ∈ J, j ∈ J , s 1 i?(j,m) ----→ s 2 , s 1 = s 2 , or i ∈ J , j ∈ J, s 1 i?(j,m) ----→ s 2 , s 1 = s 2 .
The composition operation G is commutative and associative by definition. We will thus write the product of several processes as A 1 G . . . G A n , or G i=1...n A i . Predicates and LTL Satisfaction We will use LTL for our specifications [START_REF] Pnueli | The temporal logic of programs[END_REF] which use the predicates P we consider for our model. We assume the reader is familiar with this logic, and refer to [START_REF] Pnueli | The temporal logic of programs[END_REF][START_REF] Clarke | Model Checking[END_REF] otherwise. We just need the eventually (F), and globally (G) modalities. Given an LTL formula φ, we write A |= φ if all initialized τ -paths satisfy φ.

Abstractions and Simulation A label abstraction function is defined by α : Id → Id , and α : Msg → Msg3 . This function is uniquely extended to Σ(Id, Msg) by α(τ ) = τ, α(i!(j, m)) = α(i)!(α(j), α(m)), and α(i?(j, m)) = α(i)?(α(j), α(m)). We will see examples of label abstractions later in this paper.

Lemma 1. Let A i = (S i , s i init , δ i , Σ Ji (Id, Msg)) for i ∈ [1, n], with pairwise dis- joint J i ⊆ Id, and G ∈ G(m) with ∪ i J i ⊆ {1, . . . , m}. Consider a label abstraction function α, s.t. α(J i ) ∩ α(J j ) = ∅ for all i = j ∈ [1, n]; and mappings A i of A i by α so that A i Σ J i (Id,Msg),α A i . Then, G i=1...n A i {τ } G i=1...n A i .
Notice that when A {τ } B, all LTL formulas that hold in B also hold in A (see e.g. [START_REF] Baier | Principles of model checking[END_REF]) since simulation implies trace inclusion. Thus, to prove that A satisfies a given property, it suffices to verify B.

An abstraction can also be obtained by relaxing the graph G.

Lemma 2. Consider A i = (S i , s i init , δ i , Σ Ji (Id, Msg)) for i ∈ [1, n], where J i ⊆ Id are pairwise disjoint, and G, G ∈ G(m) where ∪ i J i ⊆ {1, . . . , m}. We write G = (V, E) and G = (V, E ). If E ⊆ E , then G i=1...n A i {τ } G i=1...n A i .
Approximate Synchrony We recall the results of [START_REF] Desai | Approximate synchrony: An abstraction for distributed almost-synchronous systems[END_REF] where a finite-state scheduler is defined for concurrent processes which run a periodic action with an approximately equal period. This is the case in FTSP since all nodes run processes that wake up and execute an action with an identical nominal period T . Since each node is executed on a distinct hardware with a local clock, the observed period is only approximately equal to T . Thus, some nodes can execute faster than other nodes. In our model, we would like to include different interleavings that can be observed due to clock rate changes. Let us assume that the actual period lies in the interval [σ l , σ u ] (which contains T ). However, not all interleavings between processes can be observed. In particular, if |σ u -σ l | is small, the periods of different processes will be close, so they will be approximately synchronous: within one period of a process, another process cannot execute several periods. This restricts considerably the interleavings to be considered for model checking.

Following [START_REF] Desai | Approximate synchrony: An abstraction for distributed almost-synchronous systems[END_REF], we define a scheduler that generates at least all interleavings that can be observed during the first N periods, when the clock rates are within a given interval. We give two schedulers to model such approximately periodic behaviors. We will later instantiate these again for the particular case of FTSP. Let us consider A 1 , . . . , A n , and an additional process S which will be used to schedule processes A i . Let us add a label tick i ? to each A i , and {tick i !} 1≤i≤n to S; this models the periodic task of the node i. 4 . Let us assume that all states of A i accept a transition with tick i ?.

Real-time Scheduler We define a concrete scheduler S t which describes the executions generated by local clocks. We define S t with an infinite state space, S S = [0, σ u ] n , where the i-th component is the elapsed time since the latest execution of tick i ? in process A i . We allow two kinds of transitions that alternate. There are time elapse transitions (t 1 , . . . , t n )

τ -→ (t 1 , . . . , t n ) if for some d ≥ 0, ∀1 ≤ i ≤ n, t i = t i + d, and ∀1 ≤ i ≤ n, t i ≤ σ u . Second, we have the transition (t 1 , . . . , t n ) ticki!
----→ (t 1 , . . . , t n ) where t j = t j for all j = i and

t i = 0 if t i ∈ [σ l , σ u ].
Thus, S t describes the executions where each process is executed with a period that varies within [σ l , σ u ].

Abstract Scheduler Although the scheduler S t above describes the behaviors we are interested in, its state space is continuous, and one would need a priori timed or hybrid automata to model it precisely. In this work, we prefer using finite-state model checking techniques for better efficiency, thus we now describe a simple abstraction of S t using finite automata.

For each process i, and time t, let us denote by N i (t) the number of transitions tick i ? that was executed in A 1 . . . A n S t up to time t. We define the abstract scheduler S a (∆) on a finite state-space, given integer ∆, which ensures that, at any time point t, for all pairs of processes i, j, we have |N i (t) -N j (t)| ≤ ∆. Intuitively, S a (∆) describes the behaviors in which a fast process can execute at most ∆ periods within one period of a slow process. Notice that S a (∆) can be defined simply by counting the number of times each process has executed tick i ?. One can actually use bounded counters in [0, ∆]; in fact, it is sufficient to keep the relative values of N i (t) with respect to the smallest one, so S a (∆) can be defined as a finite automaton.

The intuition behind S a (∆) is that, given the bounds [σ l , σ u ] on the observable periods, all interleavings up to some length N under S t are also present in S a (∆). That is, S a (∆) over-approximates S t for finite executions. We will show how one can choose N . Let us denote Ticks = {tick i !} 1≤i≤n . We have the following correspondance between S t and S a : Lemma 3 ( [START_REF] Desai | Approximate synchrony: An abstraction for distributed almost-synchronous systems[END_REF]). Consider ∆ > 0, and interval [σ l , σ u ]. Let N f be the minimal integer satisfying the following constraints:

N f ≥ N s , N f -N s > ∆, σ l N f +σ u ≤ σ u N s , and N f , N s ≥ 1. Then, we have S t N f -1 Ticks S a (∆).
In the above lemma, N f represents the number of steps performed by the fastest processes, and N s is that of the slowest processes. Minimizing N f means that we look for the earliest step where N f -N s > ∆ holds, so that the simulation holds up to N f -1 steps. Hence, we can use S a (∆) for model checking rather than S t for N steps, where N is determined by ∆ and σ l , σ u .

In the FTSP, each node has a unique identifier, and the nodes dynamically elect the node with the least id as the root. The root regularly sends messages to its neighbors, which forward it to their own neighbors and so on. These messages contain time information which is used by the nodes to adjust their clocks. If the root node fails, that is, stops transmitting messages, then other nodes eventually time out and declare themselves as roots, and the protocol makes sure that a unique root is eventually elected if no more faults occur during a period of time.

More precisely, each node has an identifier ID, and executes the periodic action send, depicted in Fig. 2 in which it increments a "heart beat" counter b. This counter is reset to 0 if the node receives a certain message via the receive function: this can happen either when the node first hears about a node with a smaller ID ri than the currently known one, stored in r, or when the currently known root sends a new message with a larger sequence number si than that of the latest message s. The sequence numbers are used to distinguish new messages from the old ones that originate from a root node; a lexicographic order is used so that smaller root IDs with higher sequence numbers are preferred. A node declares itself root if the counter b exceeds the threshold FTO; and it only broadcasts messages if it is root, or if it has received at least LIM messages from some root. We refer the reader to [START_REF] Maróti | The flooding time synchronization protocol[END_REF] for the details on FTSP.

Both functions send and receive are executed atomically. Thus, the effects of each function on local variables are self-explanatory. The operation o!!(r, s) means broadcast: it is a system call to broadcast the message (r, s) to all the neighbors of the node. This operation is non-blocking: when the function send returns, the node sends the message to each neighbor in an arbitrary order. We assume the broadcast data is stored in a variable m which takes values from the set {⊥} ∪ 2 Id × Msg. Here ⊥ means that there is no ongoing broadcast, and a pair (I, m) means that processes with ids in I are still to receive the message m. That is, the operation o!!(r, s) actually just assigns the value (r, s) to local variable m.

The node can receive messages and execute receive before its own broadcast is over. We just make the following assumption on broadcasts, which is justified by the fact that the typical period of the send events is about 30 seconds [START_REF] Maróti | The flooding time synchronization protocol[END_REF].

Assumption: Any broadcast started by a node is completed before the node executes the next send event.

Concrete Model

We fix a graph G ∈ G(n) with n nodes, and set Id = {1, . . . , n}, and Msg = Id×N. In Msg, the first component of a message is the ID of the root node which has generated the message (and not the ID of the node that forwards the message), while the second component is the sequence number. Each process A i is a node in the protocol in which the variable ID is i, and executes functions receive and send of Fig. 2. We define A i = (S i , s i init , δ i , Σ {i} (Id, Msg)), with S i = V i × (2 n ∪ {⊥}) where V i are the set of valuations for all local variables. For any variable a, and state s ∈ S i , we write s(a) for the value of a in s (we also write v(a) for v ∈ V i ). The second component of a state s ∈ S i denotes whether Fig. 2: Pseudocode of the main send and receive functions in FTSP the process is currently broadcasting: if it is ⊥, there is no broadcast occurring and s(m) = ⊥; if it is I ⊆ 2 Id , then message s(m) is to be received by processes in I. We denote by s[a ← a] the state obtained from s by assigning a to a.

Since each function is executed atomically, in A i , a single transition corresponds to an uninterrupted execution of send or receive, or to a communication. For any m ∈ Msg, let us define the relation receive

i (m) ⊆ V i × V i (resp. send) as (v, v ) ∈ receive i (m) (resp. (v, v ) ∈ send i ) if,
and only if there is an execution of this function from state v to state v , when the node ID is i. These relations are functions since receive i and send i are deterministic; however, subsequent abstractions will transform these into nondeterministic programs, thus we will obtain relations instead of functions. Thus, δ i is defined as follows:

(v, ⊥) ticki? ----→ (v , N G (i)) ⇔ (v, v ) ∈ send i ∧ v (m) = ⊥, (v, ⊥) ticki? ----→ (v , ⊥) ⇔ (v, v ) ∈ send i ∧ v (m) = ⊥, (v, ∅) tocki? ----→ (v[m ← ⊥], ⊥), (v, I) j?(i,m) -----→ (v , I) ⇔ (v, v ) ∈ receive i (m) ∧ j ∈ N G (i), (v, I) i!(j,m) ----→ (v, I \ {j}) ⇔ m = v(m) = ⊥ ∧ j ∈ I,
where the last two lines are defined for all I ∈ {⊥} ∪ 2 Id .

Notice that we separate the execution of the body of the two functions and the broadcast operations. A broadcast operation is completed between the tick i ? and tock i ? events. Hence, the broadcast can be interrupted with a receive event, but another send event cannot be executed before the broadcast is complete, which conforms to our assumption above. The role of tick i and tock i signals will be clear in the next paragraph where the schedulers are defined. The initial states are the set of all valuations since we assume that the network starts in an arbitrary configuration. Now, G i=1...n A i defines the protocol on the given topology G. It remains to define the schedulers.

Schedulers and Two Communication Semantics

We define schedulers which determine when each process can execute its send event, and how the communication is modeled. We sketch our schedulers with two communication models.

Synchronous Communication

In the first model, we assume that communication between the sender and all receivers occur simultaneously. So, one step consists in a node executing send followed by all its neighbors immediately receiving the message by executing receive. This is the synchronous communication model as considered in previous works [START_REF] Kusy | Ftsp protocol verification using spin[END_REF][START_REF] Mcinnes | Model-checking the flooding time synchronization protocol[END_REF][START_REF] Tan | Analyzing the robustness of ftsp with timed automata[END_REF] To implement synchronous communication, we introduce the signal tock i !, and force the whole communication initiated by node i to happen uninterrupted between tick i ! and tock i ! signals. We define S t,syn by modifying the real-time scheduler S t defined above by requiring that each tick i ! is immediately followed by a corresponding tock i !, and by disallowing any other tick j ! inbetween. We also define S ftsp a,syn (∆) from S a (∆) using the alternating tick i and tock i signals.

Asynchronous Communication

The second type of schedulers we define implement asynchronous communication, and is more faithful to the real behavior e.g. in the TinyOS implementation. In this setting, both events send and receive are still atomic, but the broadcast is concurrent: while the sender is broadcasting the message to its neighbors, other nodes can execute their own send action or receive other messages. We call this the asynchronous communication model.

We define S t,asyn by adding to S t self-loops labeled by tock i ! to all states for all i ∈ Id. (Note that tock i ! signals are useless here, but we keep them so that both schedulers have a uniform interface). We define the scheduler S ftsp a,asyn (∆) similarly, by adding self-loop tock i ! to all states of S a (∆).

The next developments are independent from the communication model.

Complete Model and Property to be Verified Given a graph G ∈ G(n)

let A 1 , . . . , A n denote the processes thus defined, and write A(G) = G i=1...n A i . We let M conc (G) = A(G) S t, , for ∈ {syn, asyn}, which is the concrete protocol under the real-time scheduler S t defined above. This model defines the behaviors we would like to verify. For each i ∈ Id, let us add a counter c i to the model that counts the number of times tick i ! is executed, and define c = max i c i , which will be used in the specifications.

The property we want to check is that all nodes eventually agree on a common root. Let FRID denote the constant 1, which stands for the f uture r oot id. In fact, according to the protocol, A 1 is expected to become the root since it has the least id. We will call A 1 the future root. Define P i as the set of states in which the local variable r of process i has value FRID. We consider the property P(N ) = F(c ≤ N ∧ ∧ n i=1 P i ) for some N . Thus, along all executions, before any process has executed more than N tick i 's, all processes agree on FRID to be the root. Thus, our goal is to show that M conc (G) |= P(N ) for some N > 0. By Lemma 3, given ∆, it suffices to find N > 0 for each ∈{syn, asyn}, such that A(G) S ftsp a, (∆) |= P(N ).

Abstractions on Individual Nodes

We now present the abstraction steps we use before model checking. We will abstract our variables and statements involving these using data abstraction: we map the domain of the variables to a smaller set, and redefine the transitions using existential abstraction so that the abstract program is an over-approximation in the sense that the original process is simulated by the existential abstraction. This is a standard abstraction technique; we refer the reader to [START_REF] Clarke | Model checking and abstraction[END_REF] for details. More precisely, the applied abstraction steps are the following.

1. Add a redundant variable imroot that stores the value of the predicate r == ID, that is, whether the node is currently root. 2. Relax the behaviors of both functions in the case r = FRID∧ri = FRID∧ID = FRID by abstracting the variables s and e away (i.e. we assume their values change arbitrarily at any time). 3. Map the variables r and ri in the abstract domain {FRID, NRID} in each node. Also map b to the bounded integer domain {0, FTO}, e to {0, . . . , LIM}.

The resulting pseudocode is shown in Fig. 3. Here, the value ⊥ represents any value, which make any comparison operation nondeterministic. The constant NRID we introduce stands for non-root id, and is an abstract value that represents all ids different than FRID.

Note that the second step always yields an over-approximation, independently from the if-then-else condition chosen to separate the concrete and abstract cases in Fig. 3. In fact, the concrete case is identical to the original code, while the abstract case is an over-approximation by data abstraction. In Fig. 3, the abstractions of the predicates on variables r and ri are represented in quotes. They represent non-deterministic transitions as follows. The comparison relation becomes non-deterministic: we have FRID < NRID and FRID = FRID, but, for instance, a comparison between NRID and NRID can yield both true and false. As an example, "r == ri" stands for r = FRID && ri = FRID || r = NRID && ri = NRID && *, * being a nondeterministic Boolean value.

Let S i = V i × (2 n ∪ {⊥}) where V i is the set of valuations of node variables (with given id i), with the abstract domains we have described. Let us define the relations receive i ⊆ V i × V i and send i ⊆ V i × V i , similarly as before, e.g. (s, s ) ∈ receive i if, and only if there is an execution of receive i from s yielding s . Let A i denote the process defined just like A i in Subsection 3.1 but using the new relations receive i and send i . We state the relation between A i and A i using a label abstraction function α. We let α be the identity over Id, and set Msg = {FRID, NRID} × (N ∪ {⊥}) with α((k, s)) = (FRID, s) if k = FRID, and α((k, s)) = (NRID, ⊥) otherwise.

Lemma 4. For all

i, A i Σi(Id,Msg),α A i . By Lemma 1, it follows that G i=1...n A i {τ } G i=1...n A i .

Abstraction on Network Topology: Shortest-Path Abstraction

Recall that our model has a network topology G ∈ G K (n). Consider an arbitrary shortest path

A i1 A i2 . . . A im with m ≤ K, where i 1 = 1. Let C = {i 2 , . . . , i m },
that is, all nodes on this path but the future root. We need to adapt the scheduler so that it does not keep track of the offset of the processes represented by O. Let S ftsp a,syn (∆) and S ftsp a,asyn (∆) defined similarly as before which track the offsets of all nodes in C ∪ {1}, but have a self-loop with label tick O ! at all states. We thus have S ftsp a, (∆) Ticks,α S ftsp a, (∆) for both ∈ {syn, asyn}.

Define O = Id \ C. Let us relax the graph G = (V, E) into G = (V, E ) by E = E ∪ O × O ∪ O × C ∪ C × O.
/ i f ( r == FRID | | r i == FRID | | ID == FRID) { i f ( "ri < r" && ! ( b < MIN && i m r o o t ) | | "ri == r" && s i -s > 0 ) { r = r i ; s = s i ; i m r o o t = ( ID == FRID ) ; i f ( "r < ID" ) b = 0 ; i f ( e < LIM) e++; } } e l s e { / * A b s t r a c t c a s e * / i f ( "ri < r" && ! ( b < MIN && i m r o o t ) | | ( "ri == r" && * ) { r = r i ; s = ⊥ ; i m r o o t = "r == ID" ; i f ( "r < ID" ) b = 0 ; e = ⊥ ; }}}
By Lemmas 1-2, A O G A C G S ftsp a, (∆) {τ },α B O G B C G S
ftsp a, (∆). We need another abstraction to obtain a finite model: The variable s is a priori unbounded in each process; however, the only applied operations are incrementation (by FRID only), assignment, and comparison. Therefore, we can shift the values so that the minimal one is always 0; thus limiting the maximal value that is observed. We modify our process to map these variables to a finite domain {0, 1, . . . , SeqMax, ⊥} and normalize their values after each transition: we make sure that at any step, the values taken by s at all nodes define a set X ∪ {⊥} for some 0 ∈ X ⊆ {0, 1, . . . , SeqMax}.

We summarize all the steps of the abstractions as follows. Given graph

G ∈ G K (n), a path π of length K from node 1, let M abs (G, π, ∆) = B O G B C G S ftsp
a, (∆) where ∈ {syn, asyn}.

Lemma 5. For all n, K > 0, and all G ∈ G K (n), let π be any shortest path from node 1. Let C be the nodes of π except 1, and O = [1, n] \ C. We have, for all ∈ {syn, async}, M conc (G) {τ } M abs (G, π, ∆).

Notice that in M abs (G, π, ∆), all node ids are in the set {FRID, NRID}. Thus, given two different paths π, π , M abs (G, π, ∆) and M abs (G, π , ∆) are identical up to the renaming of their channel numbers since both models still contain labels of the form i!(j, m) and i?(j, m). However, these numbers i, j only define the topology and do not affect the behaviors. Let us state this formally as follows:

Lemma 6. For all K, n > 0, graph G ∈ G K (n), and paths π, π of same length from node 1, we have M abs (G, π, ∆) {τ } M abs (G, π , ∆).

From the above lemma, it follows that for verification purposes (against LTL), the model M abs (G, π, ∆) is actually independent of the chosen path π, but only depends on the length of π. For each K > 0, let us pick one such model with |π| = K and name it M abs (K, ∆). Then, we have M abs (G, π, ∆) {τ } M abs (K, ∆) for all G ∈ G K (n) and ∆ > 0. It follows that model checking a property in M abs (K, ∆) proves it on all graphs G ∈ G K (n) and all paths π.

In the rest, w.l.o.g. let us assume that C = {2, . . . , K}. Our goal is to check M abs (K, ∆) |= P K (N ) for some N , where P K (N ) = F(c ≤ N ∧ K i=1 P i ).

Incremental Verification Technique and Refinement

We explain an incremental approach to model-check our system for successive values of K. Intuitively, we assume that we have proved the root election property for K, and we want to prove it for K + 1. For K, if we prove the the property is persistent, that is, holds forever after some point in time, then, we can prove the property for K + 1 as follows: initialize the first K nodes in M abs (K + 1, ∆) to a state in which they agree on the future root, and the K + 1-th node in an arbitrary state; then verify the property for the last process only: Lemma 7. Consider processes R 1 , . . . , R n , and S 1 , . . . , S n . For some graph G, let R

(K) = G i=0...K R i . Assume that R(K + 1) G S K+1 τ R(K) G S K for all K. Consider predicate Q i for each R i , and define Q(K) = ∧ K i=1 Q i . Con- sider R (K+1) obtained from R(K+1) by restricting the states to Q(K) (That is,
we remove all states outside and all transitions that leave outside this set.), where the initial state set is Q(K). We have that R

(K) S K |= FGQ(K) ∧ R (K +1) S K+1 |= FGQ K+1 implies R(K + 1) S K+1 |= FGQ(K + 1).
Here is how we apply the above lemma in our case. Let R i = A i+1 for i = 1 . . . K. We write S K = S ftsp a,asyn (∆) defined for C = {1, . . . , K} in Section 3.3, and let S K = A O K S K with O K = Id \ {2, . . . , K}. We have A O K+1 Σ(O K+1 ,Msg ) A O K and S K+1 Ticks S K by definition, so these processes do satisfy the relation R(K + 1) S K+1 τ R(K) S K . As properties to satisfy, we consider

Q i = P i ∧ b i ≤ FTO -1 ∧ e ≥ LIM, and also define Q(K, N ) = (c ≤ N ∧ ∧ K i=1 Q i ). Notice that Q(K, N ) implies P K (N ).
Assume we have proved the following statements:

M abs (1, ∆) |= FGQ(1, n 1 ), M abs (2, ∆) |= FGQ(2, n 2 ), . . ., M abs (K -1, ∆) |= FGQ(K -1, n k-1
), and

M abs (K, ∆) |= FGQ(K, n k ).
Then, by the previous lemma, M abs (K, ∆) |= FGQ(K, N ) for N = n 1 + . . . + n k , which means P K (N ). Note that the last property to be proven can also be chosen as FP K which might be satisfied earlier than FGQ(K, n k ).

Non-interference Lemma The first verification attempts reveal a spurious counter-example: the non-deterministic process B O can send a node in C a message (r, s) with r = FRID and s large enough so that the node will ignore all messages for a long period of time, causing a timeout; this causes the violation of FGP i . However, intuitively, a node should not be able to send a message with r = FRID with a newer sequence number than what has been generated by the root itself. Following [START_REF] Chou | A simple method for parameterized verification of cache coherence protocols[END_REF], we use guard strengthening: We require that all messages that come from the process B O must satisfy that either r = FRID or s is at most equal to the variable s of the root. Let this condition be φ. We thus constrain the transitions of our model to satisfy φ, which eliminates this spurious counter-example. Property φ is also called a non-interference lemma [START_REF] Chou | A simple method for parameterized verification of cache coherence protocols[END_REF]. However, we also need to actually prove φ. As it turns out, one can prove φ on the very same abstraction obtained by strenghtening. The works [START_REF] Chou | A simple method for parameterized verification of cache coherence protocols[END_REF][START_REF] Krstic | Parameterized system verification with guard strengthening and parameter abstraction[END_REF] explain why the apparently circular reasoning is correct. We do not detail this technique further since this is now a well-known result; see also [START_REF] Talupur | Going with the flow: Parameterized verification using message flows[END_REF][START_REF] Bingham | Automatic non-interference lemmas for parameterized model checking[END_REF].

Algorithm and Experimental Results

Semi-Algorithm for FG Properties with Optimal Bound Computation Model checking algorithms consist in traversing the state space while storing the set of visited states so as to guarantee termination. However, this set can sometimes become prohibitively large. We introduce a simple semi-algorithm for properties of type FG p where we do not store all states: at iteration i, we just store the states reachable in i steps exactly, and only if all these satisfy p, do we start a fixpoint computation from these states. The resulting semi-algorithm is more efficient and allows us to find the smallest i in one shot.

We implemented the semi-algorithm in NuSMV 2.5.4 5 . We model-checked the property P(N ), and computed the bounds N using our semi-algorithm. The models are initialized in an arbitrary state, so our results show that the network recovers from any arbitrary fault within the given time bound. We summarize our results in Fig. 4. We distinguish the best values for N in both communication models for different values of K. Missing rows mean timeout of 24 hours.

We observe that the time for the root election N differs in the two communication semantics. This value is higher in the asynchronous case since it contains all behaviors that are possible in the synchronous case. Observe that the largest network topology that had been model checked for FTSP contained 7 nodes [START_REF] Mcinnes | Model-checking the flooding time synchronization protocol[END_REF] with synchronous communication. In our case, we prove the property for K = 7, which means that it holds on two dimensional grids with 169 nodes (13 × 13) when the root is at the middle (and three-dimensional grids with 2197 nodes), and 49 nodes if it is on a corner (and 343 nodes in three dimensions). In the asynchronous case, we prove the property for K = 5, e.g. 2D grids of size 81 nodes where the root is at the middle. This implies the following bounds on clock rates: by Lemma 3, for N = 107, property P(N ) is guaranteed on M conc (G) for all G ∈ G K and [σ l , σ u ] = [29.7, 30.3] which is the case when the clock rates are within 1 ± 10 -2 .

synchronous

Conclusion

We presented an environment abstraction technique inspired from [START_REF] Chou | A simple method for parameterized verification of cache coherence protocols[END_REF] for processes with unique identifiers, arbitrary network topologies, and drifting clocks. We introduced an incremental model checking technique, and gave an efficient semi-algorithm that can compute bounds for the eventually properties in one shot. We applied our technique to model check the root election part of FTSP and obtained significant improvements over previous results.

An important future work will be to automatize the presented abstraction method. Several steps of our abstractions, such as data abstractions, can easily be automatized with minimal user intervention. We would like to go further following [START_REF] Bingham | Automatic non-interference lemmas for parameterized model checking[END_REF], and consider automatic abstractions of the network topology.

Our aim is to address the case of more elaborate time synchronisation protocols based on interval methods, such as Sugihara and Gupta's [START_REF] Sugihara | Clock synchronization with deterministic accuracy guarantee[END_REF] that are able to implement TSP in WSN without making assumptions on bounded drift, but simply on precise thermal and cristal oscilator specifications of the WSN hardware. We would like to obtain formal bounds on time precision guaranteed by a protocol under various assumptions on environment.

We believe our shortest-path abstraction technique can be used to verify different distributed protocols in which an information is forwarded in layers through the network such as [START_REF] Vasudevan | Design and analysis of a leader election algorithm for mobile ad hoc networks[END_REF][START_REF] Bakhshi | Formal analysis techniques for gossiping protocols[END_REF]. An interesting future work would be to consider protocols that construct a spanning tree of the network in which case shortest paths would be replaced by a richer subgraph of the network topology.

#

  d e f i n e MAX 6 / * MAX ENTRIES * / #d e f i n e LIM 3 / * ENTRY SEND LIMIT * / #d e f i n e MIN 2 / * IGNORE ROOT MSG * / #d e f i n e FTO 8 / * ROOT TIMEOUT * / extern i n t ID / * TOS NODE ID * / #d e f i n e NIL 255 void r e c e i v e ( b y t e r i , b y t es i ) { i f ( r i < r && ! ( b < MIN && r==ID ) ) | | ( r i == r && s i -s > 0 ) { r = r i ; s = s i ; i f ( r < ID ) { b = 0 ; } i f ( e < MAX) { e ++;} } }1 b y t e b ; / * h e a r t B e a t s * / 2 b y t e e ; / * numEntries * / 3 b y t e r ; / * outgoingMsg . rootID * / 4 b y t e s ; / * outgoingMsg . seqNum * / 5 chan o ; / * Output c h a n n e l * / 6 7 void s e n d ( ) { 8 i f ( b >= FTO) { 9 i f ( r == NIL ) { s = 0 ; } 10 e l s e { b = 0 ; s ++; r == ID ) { o ! ! ( r , s ) ; s ++; } 15 e l s e i f ( e >= LIM) { o ! ! ( r , s ) } 16 }

  Thus, we render the graph complete within O, and add all edges betwen O #d e f i n e LIM 3 / * ENTRY SEND LIMIT * / #d e f i n e MIN 2 / * IGNORE ROOT MSG * / #d e f i n e FTO 8 / * ROOT TIMEOUT * / #d e f i n e NIL 255 extern i n t ID ; / * TOS NODE ID * / #d e f i n e FRID 0 / * FUTURE ROOT ID * / #d e f i n e NRID 1 / * A b s t r a c t ID f o r a l l o t h e r n o d e s > FRID * / void r e c e i v e ( b y t e r i , b y t e s i ) { / * Concrete c a s e *

1 b y tFig. 3 :

 3 Fig.3: After the second and third steps of the abstraction. The behavior of receive is relaxed when r != FRID or the received message (ri,si) is such that ri != FRID. Similarly, the behavior of send is relaxed when r != FRID and ID != FRID. For both functions, we redefine the behaviors of the protocol by disregarding the variables e and s. The updates and tests on these variables become completely non-deterministic. In particular, nodes in such states can send more often messages with arbitrary sequence numbers. Then, the variables r,ri are mapped to the domain {FRID, NRID}. The variable b is mapped to {0, 1, . . . , MAX}, and e to {0, 1, . . . , LIM}.

Fig. 4 :

 4 Fig. 4: Verification results for the property P(N ), obtained with the semi-algorithm. For each K and communication model, the best derived N is given.

Both are denoted α. Formally, α can be defined on the disjoint union of these sets.

These labels can actually be defined within Σ(Id, Msg) by adding a special message content tick to Msg, and setting ticki! = (n+1)!(i, tick) where n+1 is the identifier of S. We will write them simply as ticki? and ticki! to simplify the presentation.

The source code and models are available at https://github.com/osankur/nusmv/tree/ftsp.

A Proofs

A.1 Definitions Proof (of Lemma 1). Let A = A 1 . . . A n , and A = A 1 . . . A n . Note that the latter product is well-defined since by hypothesis α(J i ) ∩ α(J j ) = ∅.

Let S = S 1 × . . . × S n , and S = S 1 × . . . × S n . For any s ∈ S, let s i denote the i-th component, that is, s = (s 1 , . . . , s n ), and similarly for S .

Let R i denote the simulation relation that witnesses A i Σ J i (Id,Msg),α A i . We define relation R ⊆ S × S as R = {(s, s ) | ∀i, (s i , s i ) ∈ R i }. We show that R is a τ -simulation relation. The initial states are related by R by definition.

Consider any (s, s ) ∈ R, and transition s τ -→ t in A. We distinguish two cases.

-Assume δ i (s i , τ, t i ) for some i ∈ [1, n], and t j = s j for all j = i. Then, since (s i , s i ) ∈ R i , A i has some transition δ i (s i , τ, t i ), and by definining t j = t j for all j = i, (s , τ, t ) is a transition in A . -Otherwise, for some i, j ∈ Id, m ∈ Msg, δ i (s i , i!(j, m), t i ), δ j (s j , j?(i, m), t j ), and for all k = i, j, t k = s k . By R i and R j , there are t i and t j such that δ i (t i , α(i!(j, m)), t i ) and δ j (t j , α(j?(i, m)), t j ). Thus, δ (s , τ, t ) in A where t is defined by t k = t k for all k = i, j. Moreover, (t, t ) ∈ R.

Proof (of Lemma 2). This simply follows from the definition of the product. In fact, the identity relation is a simulation since any transition that is possible within G is possible in G as well.

A.2 Abstractions on Individual Nodes

Proof (of Lemma 4). Let us formally define the abstraction function abs from V i to V i described in the core of the paper. For all v ∈ V i , we define the valuation abs(v) ∈ V i as follows.

abs(v)(b) = min(b, FTO), -abs(v)(e) = min(e, LTO), -abs(v)(r) = FRID if r = 1, and NRID otherwise,

where, for the last line, recall that α((r, s)) = (α(r), s). By definition of the existential abstraction, we have

We define the relation receive i (m ) for any abstract message m ∈ α(Msg) as follows.

Let us show that the relation

Initially, we have s init × abs(s init ) ⊆ R by definition. Consider an arbitrary pair ((v, I), (u, I)) ∈ R. We consider the five types of transitions that are possible in A i .

Assume we have (v, ⊥)

ticki?

----→ (v , N i (G)) in A i , which means that (v, v ) ∈ send i . By definition of send i , we have (abs(v), abs(v )) ∈ send i . Since u = abs(v) by definition of R, we have (u, ⊥) ticki?

----→ (u , ⊥) where u = abs(v ). Thus, clearly, ((v , ⊥), (u , ⊥)) ∈ R.

The situtation is similar if (v, ⊥)

ticki?

----→ (v , ⊥). ------→ (abs(v), I \{j}) in A i since α(m) = abs(v)(m). Thus ((v, I \ {j}), (abs(v), I \ {j})) ∈ R.

Assume (v, ⊥)

Assume we have (v, I)

j?(i,m) -----→ (v , I) in A i for some j ∈ N G (i), which means that (v, v ) ∈ receive i (m). By definition of receive i (abs(m)), we have (u, abs(v )) ∈ receive i (abs(m)), so we get (u, I) j?(i,α(m))

-------→ (abs(v ), I), and (v , abs(v )) ∈ R as required.

A.3 Abstraction on Network Topology

Let us formally define S ftsp a,syn (∆). Let us write C = C ∪ {1}. Given ∆, we define the state space as ({s}

The definition is similar to S ftsp a,syn (∆) but the states s 1 , s 2 , . . . and the vector {0, 1 . . . , ∆} n are now only defined for C . The transitions are as follows.

Furthermore, we always allow self-loops with labels tick O ! and tock O !. Lemma 8. We have S ftsp a, (∆) Ticks,α S ftsp a, (∆) for all ∈ {syn, asyn}.

Proof. Let us define p 1 : {s, s 1 , . . . , s n } → {s}∪{s i } i∈C by p 1 (s) = s, p 1 (s i ) = s i for all i ∈ C , and p 1 (s i ) = s for all i ∈ C . Furthermore, let p 2 : {0, 1, . . . , ∆} n → {0, 1 . . . , ∆} C be the projection which leaves out only the components in C . We then define p((s, v))

Abstracting Sequence Numbers Recall that due to our abstraction, in B C , the sequence number s of any process has value ⊥ at all states s with s(r) = FRID. Otherwise, this value is an integer. For a given state (s i ) i∈C of B C , let α(s) = 0 if ∀i ∈ C, s(s) = ⊥, and α(s) = min i∈C,si(s) =⊥ s i (s) otherwise.

We map each state s to abs (s) by subtracting α(s) to variable s for all i ∈ C whenever s(s) = ⊥. This ensures that either all values are ⊥, or some of them is equal to 0. This will ensure that the range of these variable stay bounded. In the model, we encode these variables as bounded integers in [0, SeqMax], and check the invariant that their values stay within [0, SeqMax -1].

As an example, if we have 5 nodes in C assigning to variable s the values (3, 7, 4, ⊥, ⊥), this vector is normalized as (0, 4, 1, ⊥, ⊥).

Let B C denote the process obtained by applying abs after each transition of B C . One can show that B C and B C are bisimilar. In fact, the protocol never uses the absolute values of these numbers; the behavior only depends on comparisons between these variables, and the only allowed operation is incrementation and reset which can only be executed by the process with id FRID. ----------→ s 1 in B O . Otherwise, we must have j = i 2 since π is a shortest path. In this case, ρ(i 2 ) = i 2 and the edge (i 1 , i 2 ) is also present in H , so the corresponding transition exists in B O .

Assume i = 1. In this case, there exists states s, s such that abs (s) = (s 1 , v) and abs(s ) = (s 1 , v ), and

----→ s i . We have m = (r, s) such that s ≤ v by definition of the abstraction. Let i ∈ O \ {1}. One can define states t, t such that abs (t) = (s 1 , v) and abs (t ) = (s 1 , v ), and

The case of receive transitions are proven similarly.

We show B C ∼ Id(Id,Msg ),ρ B C in a similar way. We write the states of A C as a product of S C = S i1 × . . . × S i K , and those of B C as S C = S i 1 × . . . × S i K . We consider again the identity relation to be shown to be a simulation. As before, τ -transitions trivially match. Let s ∈ S C , and consider s

Assume j ∈ O \ {1}. In this case, we have ρ(i l ) = i l and the edge (ρ(i l ), ρ(j))

exists in H . Thus, the transition s i l !(ρ(j),m)

-------→ s exists in B O . Assume j = i l with l = l + 1 or l = l -1 since π is a shortest path. In this case, ρ(i l ) = i l , and ρ(i l ) = i l , and the edge is present in H ; so the corresponding transition exists in B O .

The case of receive transitions are proven similarly.

The same reasoning applies to the scheduler which is connected to all nodes.

Proof (of Lemma 7).

means that all runs of R(K + 1) S K+1 that start anywhere in Q(K) and remain within eventually reach and stay in Q K+1 , thus also in Q(K + 1). Putting the two properties together, we get that all runs of R(K + 1) S K+1 eventually reach and stay in Q(K + 1), that is to say, R(K + 1) S K+1 |= FGQ(K + 1).

B Schedulers

Synchronous Real-time Scheduler The scheduler S ftsp t,syn is defined as follows. The state space is {s, s 1 , . . . , s n } × [0, σ u ] n . We add delay transitions only when the first component is in s: (s, (t 1 , . . . , t n )) τ -→ (s, (t 1 , . . . , t n )) if for some d ≥ 0, ∀1 ≤ i ≤ n, t i = t i +d, and ∀1 ≤ i ≤ n, t i ≤ σ u . Otherwise time does not progress.

We have the transition (s, (t 1 , . . . , t n )) ticki! ----→ (s i , (t 1 , . . . , t n )) where t j = t j for all j = i and t i = 0 if t i ∈ [σ l , σ u ], and we let (s i , (t 1 , . . . , t n )) tocki! ----→ (s, (t 1 , . . . , t n )).

Asynchronous Real-time Scheduler The scheduler S ftsp t,asyn is defined on the state space [0, σ u ] n . The only difference with S ftsp t,syn is that we do not have the extra component {s, s 1 , . . . , s n } and tock i ! transitions are always allowed.

Formally, delay transitions are allowed with the following condition

We have the transition (t 1 , . . . , t n ) ticki! ----→ (t 1 , . . . , t n ) where t j = t j for all j = i and

Abstract Synchronous Scheduler Let us now define the abstract scheduler S ftsp a,syn (∆). To implement approximate synchrony, let us define a variable offset i for each i ∈ Id. Given parameter ∆, we define the state space as {s, s 1 , . . . , s n }×{0, 1, . . . , ∆} n ; thus the state consists in control state among s, s 1 , . . . , s n and in a valuation for offset i . The initial state is (s, 0). Intuitively, the offset i variable contains the information on the number of times tick i ! was executed since the beginning, except that we only store the value relative to the smallest one. The transitions are as follows. For all i ∈ Id,

The first transition ensures that the offset is always bounded by ∆, thus making the state space finite. In fact, we make sure the smallest offset is always 0. Notice that once the scheduler sends a tick i ! signal, it can send another tick j ! only after doing tock i !. This is what makes sure that the semantics is synchronous: the broadcast must be completed before any other node wakes up. We will later choose ∆ and justify its choice.

Abstract Asynchronous Scheduler

We define S ftsp a,asyn (∆) on the state space is {s} × {0, 1, . . . , ∆} n ; and the transitions are, for all i ∈ Id,

Thus, the scheduler is allowed to send other tick j ! signals regardless whether tock i ! has been done.

C Intermediate Abstraction Steps

We give, in Fig. 5 the send and receive functions in which the redundant predicate imroot is added.

D Semi-Algorithm to check FG p Properties

We describe our semi-algorithm in more detail. Given a set of states R, let Post(R) denote the set of states reachable from R in one transition. At each step i, we compute Post i (Init) where Init is the set of initial states. Note that we do not keep in memory previously computed sets Post j (Init) with j < i. We check whether Post i (Init) ⊆ p. If this does not hold, we continue the iteration by incrementing i. In fact, in this case, the property FG p cannot hold for all states from step i. If this does hold, then we compute all the states reachable from Post i (Init): ∪ j≥i Post j (Init). If this set is included in p, then we have proven the property, which holds starting from step i. If at any moment, it turns out that Post j (Init) ∩ p = ∅, then our guess was wrong; we set i = j, and continue. Now, if there exists a number i such that all executions satisfy Gp starting from step i, then this semi-algorithm terminates; otherwise, it might not terminate. The advantage however, is that while we are looking for this number i, we only store Post i (Init) so the memory usage is reduced; and moreover, BDD reorderings can be used much more efficiently since the BDD cache is much smaller.