# A Formal Approach to Verify Parameterized Protocols in Mobile Cyber-Physical Systems

Authors: Long Zhang; Wenyan Hu; Wanxia Qu; Yang Guo; Sikun Li
Journal: Mobile Information Systems
 (2017)

---

## Abstract

Mobile cyber-physical systems (CPSs) are very hard to verify, because of asynchronous communication and the arbitrary number of components. Verification via model checking typically becomes impracticable due to the state space explosion caused by the system parameters and concurrency. In this paper, we propose a formal approach to verify the safety properties of parameterized protocols in mobile CPS. By using counter abstraction, the protocol is modeled as a Petri net. Then, a novel algorithm, which uses IC3 (the state-of-the-art model checking algorithm) as the back-end engine, is presented to verify the Petri net model. The experimental results show that our new approach can greatly scale the verification capabilities compared favorably against several recently published approaches. In addition to solving the instances fast, our method is significant for its lower memory consumption.


---

## Body

## 1. Introduction

A cyber-physical system (CPS) [1] is an integration of computation and physical components. The improvement of contemporary mobile devices, such as smartphones and wearable electronics, enables the formation of mobile CPSs [2, 3]. A mobile CPS could be considered as a subcategory of CPSs with inherent mobile features [4, 5]. Different from traditional CPSs, mobile CPSs could be built on mobile devices that travel with their owners. For example, mobile social networking [6, 7] helps people communicate with each other on their daily commute to and from work, traveling along the same rotes at about the same time. Due to distributed interactions of cyber word, physical word, and human behaviors, the mobile CPS becomes more complex. Asynchronous communication and the arbitrary number of components make the mobile CPS appear similar to a parameterized system. It is difficult to guarantee the parameterized system’s correctness for any natural number [8, 9].Due to the tight market windows and safety-critical nature of their applications, it has become an urgent need to design error-free mobile CPSs and thus a significant amount of time is spent on ensuring the correctness of mobile CPS designs. The verification of the CPS designs becomes an important issue [10]. Formal methods, replacing the traditional testing methods for large mobile CPSs, have been successfully used for verifying software, hardware, and physical systems in the past decades [11]. Model checking [12, 13] is an automatic formal approach to verify if the specification satisfies the properties and has been used in finite and infinite state system verification successfully.Abstraction [14, 15] is a good way to reduce the state space. By abstraction, each agent of the mobile CPS can be modeled as a finite state automaton in which local transitions model one of the following: an internal action, a broadcast, or a reception of a message. A mobile CPS is defined as the composition of a finite but arbitrary number of copies of the automaton running in parallel. A mobile CPS which combined with an arbitrary number of components is a parameterized system, which is a wide class infinite system, including cache coherence protocols and mutual exclusion protocols.Parameterized systems arise naturally in the modeling of mutual exclusion algorithms, distributed protocols, or cache coherence protocols. Parameterized verification [8] is aimed at verifying families of transition systems for all values of the parameter. Counter abstraction [14] is natural to model parameterized systems into Petri nets and their extensions. Petri net is a powerful mathematical tool and has been used widely for modeling and verifying CPSs [10, 16, 17].In this paper, we propose a formal approach to verify the safety properties of parameterized protocols in mobile CPSs. By using counter abstraction, the protocols of mobile CPSs are described as Petri nets, and then the state-of-the-art model checker is used to check the safety properties.The significant contributions of this paper are as follows:(i)
We propose a new method based on the SAT-based model checking algorithm to verify the parameterized protocols of mobile CPSs. By using counter abstraction, we describe the parameterized protocol as a Petri net and then translate it into a finite state machine (FSM), so that IC3 [18, 19], the state-of-the-art finite state model checking algorithm, can be used as the back-end engine.(ii)
A smart encoding technique is introduced to make the verification efficient. A bounded Petri net is transformed into a FSM and described as a general format for most model checkers.(iii)
To improve the scalability of parameterized protocols verification, an incremental algorithm is proposed to make IC3 perform more efficiently.The rest of this paper is organized as follows. In Section2, we review the related work. Section 3 presents necessary preliminaries used in this paper. In Section 4, we propose our new method based on the model checking algorithm and give more details of the implementation and optimization. Section 5 shows the experimental evaluation on parameterized protocols. Section 6 concludes this paper and discusses future works.


## 2. Related Works

As a successful application in traditional hardware and software verification, model checking has been frequently used in CPS verification, especially for safety-critical CPSs. Akella and McMillin [20] encoded the physical system into an event-based discretized system and modeled the associated CPS by Security Process Algebra. The model checker, CoPS, was used to check the confidentiality properties. A statistical model checker has been recently utilized to analyze some aspects of CPSs [21]. However, this method also suffers from the classical model checking problems, such as the state space explosion and the lack of ability to reason about mathematical relations. Bae et al. [22] combined model checking and Multirate PALS (physically asynchronous, logically synchronous) methodology for the first time to verify an airplane turning control system. More cases should be studied for the verification of distributed cyber-physical systems using Multirate PALS.Petri nets are well-known tools for modeling and verification of distributed systems and CPSs. Xu and Deng [16] proposed a Petri nets-based method for architectural modeling of mobile agent systems. Chen et al. [17] investigated the use of Petri nets for modeling coordinated cyber-physical attacks on the smart grid. A novel hierarchical method was proposed to construct large Petri nets from a number of smaller Petri nets that can be created separately by different domain experts. Vita [23, 24], which is a novel mobile cyber-physical system for crowdsensing applications, introduced Petri nets to design a high level service state synchronization mechanism to address the possible unavailable situations of mobile devices in mobile CPSs. In order to define the functionality of traveler information systems (TIS) and integrate new functions and technologies based on cloud computing and mobile communications, Nemtanu et al. [25] presented a Petri nets-based model of this system. Zhang et al. [26] proposed a mechanism to model fault tolerated mobile agents by using colored Petri nets.There is a large amount of related works on automating the parameterized verification problem [27–29]. The theorem prover PVS, for example, has been successfully applied to verify Small Aircraft Transportation System (SATS) [30]. By using the Model Checker Modulo Theories, Johnson and Mitra presented a model checking method for SATS [31]. Guo et al. [32, 33] proposed a new method to reduce the state space of parameterized systems by two-dimensional abstraction (TDA). Asynchronous composition was the key part of TDA but suffered from higher memory consumption.


## 3. Preliminaries

Petri nets have been popular models for various types of asynchronous or concurrent processes. A Petri net is a directed graph consisting of places (drawn as circles), transitions (typically boxes), and directed arcs. Input places point to a transition, and a transition points to output places. A number of tokens move around the net from place to place, and the distribution of tokens among the places (called themarking) represents the dynamic state of the entire modeled system. The formal definition of Petri nets is as follows.Definition 1 (Petri net).
A Petri net (PN) is a triplePN=P,T,F, where P is a finite set of places, T is a finite set of transitions disjoint from P, and F:P×T∪T×P→N is flow relations for the set of arcs.The configuration ofPN is markings, which can be seen as the multisets of places. The semantics of PN is given by markings. Amarking is a function m:P→N, which describes the number of tokens mp in place p∈P. In the sequel, if places are ordered by P=p1,p2,…,pn, we often identify m and the vector mp1,mp2,…,mpn.Example 2.
As shown in Figure1, a simple example contains all components of a Petri net. There are two places and three transitions. Arcs have capacity 1 by default; if other than 1, the capacity is marked on the arc. Places have infinite capacity, and transitions have no capacity and cannot store tokens at all. The current marking is 1,0. If t1 is fired, the next marking will be 2,0. If t2 is fired, the next marking will be 0,1. The transition t3 cannot be fired now.Figure 1
A Petri net with two places and three transitions.In particular, it has been shown that certain communication procedures, which are common when programming distributed systems, can easily be modeled by plain Petri nets, but other communication procedures such as broadcast are not easily captured by plain Petri nets. For that reason, we address two extensions of the model in this paper, following the definition in [34].(i)
Petri nets with transfer arcs, in which a transition can also consume all tokens present in one place and move them to another(ii)
Petri nets with reset arcs, in which a transition can delete all tokens present in one placeThis significance of these extensions in terms of modeling power has been demonstrated, for instance, in the modeling and verification of parameterized protocols in [35].A common way to model a parameterized system by a Petri net is to apply the idea of the counter abstraction [8]. This principle consists of mapping each single process to a token and representing each state of each type of process by a place. In this case, the presence of a token in a given place p∈P indicates that, in the current global state of the system, there is a process that corresponds to p in its local states. The transition of the Petri net then consumes and produces tokens to move the associated process from one state to another. This formalization has the drawback of abstracting away the actual identities of the processes. Still, some interesting properties, for instance, safety properties, can be verified at this level of abstraction.In this paper, we focus on the safety property, which is equal to the coverability of well-structured transition systems (WSTSs) when expressing the safety property as the upward-closed set. Petri nets are WSTSs (with respect to ≤) [36]. We present the related notions of WSTSs and then define the PN safety problem.Definition 3 (well-quasi-ordering).
A well-quasi-ordering (wqo) is a reflexive and transitive binary relation⪯ over set X, and for every infinite sequence x0,x1,x2,… of elements from X, there exists i<j such that xi⪯xj. For Y⊆X, the upward-closure of Y is the set ↑Y=x∣∃y∈Y,y⪯x. A set U is said to be ⪯-upward-closed (or simply upward-closed if ⪯ is clear from the context) if U = ↑U.In Figure1, the safety property is defined whether the tokens number of place p2 is greater than or equal to 2; then we can use the upward-closed set p2≥2 to express the property.Definition 4 (well-structured transition systems).
A well-structured transition system (WSTS) is a transition system equipped with a wqo on its states that satisfies the monotonicity property. A WSTS is a triple(S,→,⪯) such that (1)
S is the (possibly infinite) state space,(2)
→⊆S×S is transition relation,(3)
⪯ is a wqo over S,(4)
for allx,x′,y∈S, if x→x′ and x⪯y, there exists y′ such that y→y′ and x′⪯y′.The covering relation ≤ between Petri net markings is a wqo. APN=P,T,F and the initial marking m0 give rise to a WSTS S,I,→,≤, where S is the set of markings and I corresponding with m0 is the initial states. The transition relation is defined as follows: there is an edge m→m′ if and only if there is some transition t∈T such that when transition t was fired, the marking m yields a new marking m′. The coverability problem for PN is defined as the coverability problem on this WSTS.Definition 5 (PN safety problem).
Given a Petri netPN=P,T,F and the initial marking m0, we get a WSTS S,I,→,≤. Then given an ≤-upward-closed set U⊆S, does there exist a sequence x0→x1→⋯→xl such that x0∈I and xl∈U? We write safePN,I,U if the answer is “no.”Example 6.
As shown in Figure1, if the initial marking is m0=1,0, and the safety property is described by the upward-closed set p2≥2, there exists a sequence 1,0→2,0→1,1→0,2, which means the Petri net is notsafe.


## 4. Incremental Bounded Model Checking Algorithm

This section describes how to bound a Petri net to an equivalent FSM and then verifies the safety properties by using SAT-based model checkers. An incremental method is proposed, which benefits more from the modern SAT solver by assumption.


### 4.1. Cut Off the Petri Net to FSM

In general, Petri nets are infinite state systems, as the number of tokens can be assigned with arbitraryn∈N. In order to use the finite state model checking algorithms, we cut off the Petri net to FSM by a given boundary B∈N. As the counter abstraction is used to model the parameterized systems, the boundary B can be defined as the current process number.Definition 7 (finite state machine).
A finite state machine is a quadrupleM=S,R,S0,In, where S is a finite set of states, R⊆S×S is the transition relations, S0⊆S is the initial states, and In is a finite set of inputs.To cut off the Petri net to FSM, we represent Petri nets as follows. LetP=p1,p2,…,pn be the set of places. A marking m is represented as the tuple of natural numbers m(p1),m(p2),…,m(pn). A transition t is represented as a pair (g,e)∈Nn×Nn, where g is the guards and e is the effects. Formally, g=Fp1,t,Fp2,t,…,Fpn,t, which represents the enabling condition, and e=Ft,p1,Ft,p2,…,Ft,pn, which represents the yield marking m′.The Petri net is a concurrent model, in which just one transition can be fired at one time. In the equivalent FSM, we introduce extra inputs to simulate and select one transition to be fired randomly.Definition 8 (B-bounded Petri net, B-bounded upward-closed set).
Given a Petri netPN=(P,T,F) and a boundary B∈N, a B-bounded Petri net PNB is a FSMS,R,S0,In, where S is the subset for all markings, so that, for a marking m, m(pi)≤B for all 1≤i≤n; R is the subset of T, so that, for t=(g,e)∈T, the guard g can be fired under the boundary B; S0 is the bounded initial marking m0; In is the set of extra inputs for selecting which rule to be fired. Given an upward-closed set U, UB is the B-bounded upward-closed set, which cuts off the infinite U to finite UB by the boundary B.B is the total token’s boundary, so the summary of each place’s token number should be less than or equal to B. Here an adder is used to count the total tokens, which will be discussed in Section 4.3.The bad states are presented with an upward-closed setU in Petri nets. We bound U with the boundary B, by cutting off the upward-closed set with B. For instance, for an upward-closed set p2≥2, and the boundary 10, the bounded upward-closed set is 2≤p2≤10.Here, we introduce a functioncut-off∗,B to map the Petri net PN or upward-closed set U to B-bounded Petri net or B-bounded upward-closed set. That is to say, PNB =cut-off(PN,B), and UB =cut-off(U,B).


### 4.2. SAT-Based Model Checking Algorithms for Petri Nets

The Boolean Satisfiability (SAT) problem is a well-known NP-complete constraint satisfaction problem. With the introduction of bounded model checking (BMC) [37], it becomes clear that SAT solvers can be used for model checking [12]. There has been significant progress on SAT-based model checking techniques in the past two decades, including BMC, interpolation [38], and IC3.IC3, known also as property directed reachability (PDR), is a recently proposed SAT-based model checking technique for the analysis of sequential circuits. IC3 maintains a list of trace:R0,R1,…,RN. The first element R0 is special; it is simply identified with the initial states. For k>0, Rk is a set of clauses that represents an overapproximation of the states reachable from the initial states in k steps or less. Together with the trace, the IC3 algorithm consists of a set of proof-obligations, which consists of a frame number k and a cube s. By manipulating the trace and the set of proof-obligations, IC3 gets new facts and adds them into the trace until it either (1) produced an inductive invariant proving the property or (2) added a proof-obligation at frame 0 with a cube that intersects the initial states, which is a counterexample. Without unrolling the model, IC3 performs better than most SAT-based model checking algorithms, especially in memory consumption.Given a Petri net model PN, the safety propertyU, and the boundary B∈N, U is expressed as an upward-closed set, and B is the current process number of the parameterized system to be verified. By Definition 8, we create the bounded Petri net model and bounded upward-closed set by the function cut-off(∗,B). PNB is a FSM and can be translated into propositional logic directly. UB represents the safety property for PNB. An SAT-based model checker is used to check the property. There are multiple choices of model checkers. Here the state-of-the-art model checker IC3 was used as the back-end engine, because of its lower memory consumption. If the model checker returns UNSAT, it means PN is safe for the current boundary B; otherwise, a counterexample will be found.We note this method asB-bounded model checking algorithm. Because of the use of finite state model checking algorithms, the B-bounded model checking algorithm will terminate when we find a counterexample or prove the safety.For parameterized verification problem, we want to verify the system on an arbitrary parameter. If the maximum process number isM, we need M times single runs for 1≤B≤M. For each single run, the FSM is encoded into a new propositional formula to use an SAT solver, separately.Fortunately, the modern SAT solver supports the incremental mechanism, so that the new SAT problem can be solved based on the previous solve result. The back-end SAT engine used in this paper isminisat [39], which supports the incremental mechanism by assumption. There is a vector to store the assumption variables which will be assigned toTrue. Hence, we introduce some extra variables, named active literals, to control the boundary of the bounded Petri net model.Definition 9 (Inc-bounded Petri net, Inc-bounded upward-closed set).
Given a Petri netPN=P,T,F, a boundary n∈N, and a maximum boundary m∈N, an Inc-bounded Petri net PNn→m is a m-bounded Petri net PNm equipped with the active literals vector v for controlling the boundary incrementally. An Inc-bounded upward-closed set Un→m is a m-bounded upward-closet set Um equipped with v.Ifv=an+1,an+2,…,am, the current boundary is n. If an+1 is popped out, the boundary increases to n+1. If v=∅, the boundary reaches the maximum boundary m. A new functioninc-cut-off(∗,n,m) is introduced to map the Petri net PN or upward-closed set U to Inc-bounded Petri net or Inc-bounded upward-closed set. We write that PNn→m =inc-cut-offPN,n,m, and Un→m =inc-cut-offU,n,m.Algorithm1 shows our new algorithm to verify the bounded Petri net from boundary n to m incrementally. The inputs are a Petri net model PN, safety property U, a base boundary n, and a maximum boundary m. U is expressed as an upward-closed set. The algorithm returnsunsafe if it finds a counterexample; otherwise, it returnssafe and proves the system is safe from parameters n to m.Algorithm 1:Incremental bounded model checking algorithm.
Input:
PN: a Petri net model to describe the parameterized protocol
U: an upward-closed set to describe the safety property
n: base boundary
m: maximum boundary
Output:
safe or unsafe
(1) initial assumption vectorv≔⌀ // push all active literals into assumption vector
(2)fori≔m;i>n;i≔i-1do
(3)v.push(ai)
(4)end for
(5)i≔n   // the initial boundary is n
(6)PNn→m≔  inc-cut-offPN,n,m // create the incremental bounded Petri net
(7)Un→m≔  inc-cut-offU,n,m
(8)whilev≠⌀do
(9) // use an SAT-based model checker to verify the property at the boundaryi
(10)ifPNn→m∣=Un→mthen
(11)  print CEX
(12)  RETURNunsafe
(13)else
(14)  print “PN is safe for current boundaryi”
(15)v.pop() // the boundary is increased by 1
(16)i≔i+1
(17)end if
(18)end while
(19) RETURNsafeLines 1–5. Generate the active literals and push them into the assumption vector v. Then, set the current boundary as n.Lines 6-7. Create the incremental bounded Petri net model by using the assumption vector v.Lines 8–19. The while-loop is the main routine to verify the model incrementally. If the condition is satisfied at line 10, the model checker finds a counterexample and returnsunsafe. If the model bounded by i is safe, then the algorithm increases the boundary at lines 15 and 16 and calls the SAT-based model checker again to solve the new model with higher boundary. When vector v is empty, the algorithm proves that the input PN is safe from boundaries n to m.Algorithm1 reuses the context from the previous solving results. The main routine in Algorithm 1 is based on an SAT-based model checker. Hence, the algorithm terminates when it finds a counterexample at line 12 or proves safety at line 19.


### 4.3. Implementation and Optimization

In this section, we introduce key points which make a great contribution in improving the performance.The Petri Net Format. The input Petri net is encoded in the MIST format (https://github.com/pierreganty/mist/). Each place is mapped to a variable, and each transition corresponds to a rule. For each rule, there are guards and effects, as described in Definition 8. The guards are the conditions under which this rule can be fired, and the effects describe how tokens transfer from places. The target is the safety property to be verified, which is expressed as an upward-closed set.The FSM Format. AIGER (http://fmv.jku.at/aiger/) is a format, library, and set of utilities for And-Inverter Graphs (AIGs). The hardware model checking competition (HWMCC) uses AIGER as input format, and most modern model checkers support AIGER as the input model. AIGER is a good way to describe FSM and can be translated into a propositional logic for an SAT solver. The bounded Petri net is encoded as an AIGER model, where each place corresponds to state variables in Boolean value. Extra input variables are introduced to select which rule to be fired and then update the state variables to set up the transition relations equally.Encoding: Binary versus Unary. Encoding is important for SAT solvers. In this paper, both binary and unary encodings were used to encode the places in the Petri net model. As shown in Table 1, binary and unary encodings are used to encode the natural numbers. One-hot encoding is one possible unary encoding, where just one bit is “1” and the others are all “0.” The binary encoding needs ⌈log2⁡N⌉ bits, and the unary encoding needs N bits to encode the natural number 0~N.Table 1
Encoding: binary versus unary.
n
Binary
One-hot
0
000
00000001
1
001
00000010
2
010
00000100
3
011
00001000
4
100
00010000
5
101
00100000
6
110
01000000
7
111
10000000Full Adder. A full adder is designed to count the total token numbers to bound the Petri net. As binary and unary encodings are used to represent the token numbers for each place, we present how to design an n-bit binary and unary full adder, respectively.An-bit binary full adder is just combing n single 1-bit binary adders together. The 1-bit binary adder can be described using the following logics. The logics AND, OR, and XOR are represented as ∧, ∨, and ⊕, respectively.(1)S=A⊕B⊕CinCout=A∧B∨Cin∧A⊕BThere are many different ways to design unary adder, but a simplen-bit unary adder is presented as follow:(2)Si=⋀j=0iAj∧Bi-j,0≤i<n.Structural Information. When using unary encoding to represent the token’s number of places, it is important to give this structural information to the SAT solver. Hence, we add some extra logics as a constraint to the AIGER circuits. Figure 2 shows the logics to check if the n-bit vector x is encoded in one-hot. The total number of gates is 3∗n+2.Figure 2
One-hot encoding checking logics.


## 4.1. Cut Off the Petri Net to FSM

In general, Petri nets are infinite state systems, as the number of tokens can be assigned with arbitraryn∈N. In order to use the finite state model checking algorithms, we cut off the Petri net to FSM by a given boundary B∈N. As the counter abstraction is used to model the parameterized systems, the boundary B can be defined as the current process number.Definition 7 (finite state machine).
A finite state machine is a quadrupleM=S,R,S0,In, where S is a finite set of states, R⊆S×S is the transition relations, S0⊆S is the initial states, and In is a finite set of inputs.To cut off the Petri net to FSM, we represent Petri nets as follows. LetP=p1,p2,…,pn be the set of places. A marking m is represented as the tuple of natural numbers m(p1),m(p2),…,m(pn). A transition t is represented as a pair (g,e)∈Nn×Nn, where g is the guards and e is the effects. Formally, g=Fp1,t,Fp2,t,…,Fpn,t, which represents the enabling condition, and e=Ft,p1,Ft,p2,…,Ft,pn, which represents the yield marking m′.The Petri net is a concurrent model, in which just one transition can be fired at one time. In the equivalent FSM, we introduce extra inputs to simulate and select one transition to be fired randomly.Definition 8 (B-bounded Petri net, B-bounded upward-closed set).
Given a Petri netPN=(P,T,F) and a boundary B∈N, a B-bounded Petri net PNB is a FSMS,R,S0,In, where S is the subset for all markings, so that, for a marking m, m(pi)≤B for all 1≤i≤n; R is the subset of T, so that, for t=(g,e)∈T, the guard g can be fired under the boundary B; S0 is the bounded initial marking m0; In is the set of extra inputs for selecting which rule to be fired. Given an upward-closed set U, UB is the B-bounded upward-closed set, which cuts off the infinite U to finite UB by the boundary B.B is the total token’s boundary, so the summary of each place’s token number should be less than or equal to B. Here an adder is used to count the total tokens, which will be discussed in Section 4.3.The bad states are presented with an upward-closed setU in Petri nets. We bound U with the boundary B, by cutting off the upward-closed set with B. For instance, for an upward-closed set p2≥2, and the boundary 10, the bounded upward-closed set is 2≤p2≤10.Here, we introduce a functioncut-off∗,B to map the Petri net PN or upward-closed set U to B-bounded Petri net or B-bounded upward-closed set. That is to say, PNB =cut-off(PN,B), and UB =cut-off(U,B).


## 4.2. SAT-Based Model Checking Algorithms for Petri Nets

The Boolean Satisfiability (SAT) problem is a well-known NP-complete constraint satisfaction problem. With the introduction of bounded model checking (BMC) [37], it becomes clear that SAT solvers can be used for model checking [12]. There has been significant progress on SAT-based model checking techniques in the past two decades, including BMC, interpolation [38], and IC3.IC3, known also as property directed reachability (PDR), is a recently proposed SAT-based model checking technique for the analysis of sequential circuits. IC3 maintains a list of trace:R0,R1,…,RN. The first element R0 is special; it is simply identified with the initial states. For k>0, Rk is a set of clauses that represents an overapproximation of the states reachable from the initial states in k steps or less. Together with the trace, the IC3 algorithm consists of a set of proof-obligations, which consists of a frame number k and a cube s. By manipulating the trace and the set of proof-obligations, IC3 gets new facts and adds them into the trace until it either (1) produced an inductive invariant proving the property or (2) added a proof-obligation at frame 0 with a cube that intersects the initial states, which is a counterexample. Without unrolling the model, IC3 performs better than most SAT-based model checking algorithms, especially in memory consumption.Given a Petri net model PN, the safety propertyU, and the boundary B∈N, U is expressed as an upward-closed set, and B is the current process number of the parameterized system to be verified. By Definition 8, we create the bounded Petri net model and bounded upward-closed set by the function cut-off(∗,B). PNB is a FSM and can be translated into propositional logic directly. UB represents the safety property for PNB. An SAT-based model checker is used to check the property. There are multiple choices of model checkers. Here the state-of-the-art model checker IC3 was used as the back-end engine, because of its lower memory consumption. If the model checker returns UNSAT, it means PN is safe for the current boundary B; otherwise, a counterexample will be found.We note this method asB-bounded model checking algorithm. Because of the use of finite state model checking algorithms, the B-bounded model checking algorithm will terminate when we find a counterexample or prove the safety.For parameterized verification problem, we want to verify the system on an arbitrary parameter. If the maximum process number isM, we need M times single runs for 1≤B≤M. For each single run, the FSM is encoded into a new propositional formula to use an SAT solver, separately.Fortunately, the modern SAT solver supports the incremental mechanism, so that the new SAT problem can be solved based on the previous solve result. The back-end SAT engine used in this paper isminisat [39], which supports the incremental mechanism by assumption. There is a vector to store the assumption variables which will be assigned toTrue. Hence, we introduce some extra variables, named active literals, to control the boundary of the bounded Petri net model.Definition 9 (Inc-bounded Petri net, Inc-bounded upward-closed set).
Given a Petri netPN=P,T,F, a boundary n∈N, and a maximum boundary m∈N, an Inc-bounded Petri net PNn→m is a m-bounded Petri net PNm equipped with the active literals vector v for controlling the boundary incrementally. An Inc-bounded upward-closed set Un→m is a m-bounded upward-closet set Um equipped with v.Ifv=an+1,an+2,…,am, the current boundary is n. If an+1 is popped out, the boundary increases to n+1. If v=∅, the boundary reaches the maximum boundary m. A new functioninc-cut-off(∗,n,m) is introduced to map the Petri net PN or upward-closed set U to Inc-bounded Petri net or Inc-bounded upward-closed set. We write that PNn→m =inc-cut-offPN,n,m, and Un→m =inc-cut-offU,n,m.Algorithm1 shows our new algorithm to verify the bounded Petri net from boundary n to m incrementally. The inputs are a Petri net model PN, safety property U, a base boundary n, and a maximum boundary m. U is expressed as an upward-closed set. The algorithm returnsunsafe if it finds a counterexample; otherwise, it returnssafe and proves the system is safe from parameters n to m.Algorithm 1:Incremental bounded model checking algorithm.
Input:
PN: a Petri net model to describe the parameterized protocol
U: an upward-closed set to describe the safety property
n: base boundary
m: maximum boundary
Output:
safe or unsafe
(1) initial assumption vectorv≔⌀ // push all active literals into assumption vector
(2)fori≔m;i>n;i≔i-1do
(3)v.push(ai)
(4)end for
(5)i≔n   // the initial boundary is n
(6)PNn→m≔  inc-cut-offPN,n,m // create the incremental bounded Petri net
(7)Un→m≔  inc-cut-offU,n,m
(8)whilev≠⌀do
(9) // use an SAT-based model checker to verify the property at the boundaryi
(10)ifPNn→m∣=Un→mthen
(11)  print CEX
(12)  RETURNunsafe
(13)else
(14)  print “PN is safe for current boundaryi”
(15)v.pop() // the boundary is increased by 1
(16)i≔i+1
(17)end if
(18)end while
(19) RETURNsafeLines 1–5. Generate the active literals and push them into the assumption vector v. Then, set the current boundary as n.Lines 6-7. Create the incremental bounded Petri net model by using the assumption vector v.Lines 8–19. The while-loop is the main routine to verify the model incrementally. If the condition is satisfied at line 10, the model checker finds a counterexample and returnsunsafe. If the model bounded by i is safe, then the algorithm increases the boundary at lines 15 and 16 and calls the SAT-based model checker again to solve the new model with higher boundary. When vector v is empty, the algorithm proves that the input PN is safe from boundaries n to m.Algorithm1 reuses the context from the previous solving results. The main routine in Algorithm 1 is based on an SAT-based model checker. Hence, the algorithm terminates when it finds a counterexample at line 12 or proves safety at line 19.


## 4.3. Implementation and Optimization

In this section, we introduce key points which make a great contribution in improving the performance.The Petri Net Format. The input Petri net is encoded in the MIST format (https://github.com/pierreganty/mist/). Each place is mapped to a variable, and each transition corresponds to a rule. For each rule, there are guards and effects, as described in Definition 8. The guards are the conditions under which this rule can be fired, and the effects describe how tokens transfer from places. The target is the safety property to be verified, which is expressed as an upward-closed set.The FSM Format. AIGER (http://fmv.jku.at/aiger/) is a format, library, and set of utilities for And-Inverter Graphs (AIGs). The hardware model checking competition (HWMCC) uses AIGER as input format, and most modern model checkers support AIGER as the input model. AIGER is a good way to describe FSM and can be translated into a propositional logic for an SAT solver. The bounded Petri net is encoded as an AIGER model, where each place corresponds to state variables in Boolean value. Extra input variables are introduced to select which rule to be fired and then update the state variables to set up the transition relations equally.Encoding: Binary versus Unary. Encoding is important for SAT solvers. In this paper, both binary and unary encodings were used to encode the places in the Petri net model. As shown in Table 1, binary and unary encodings are used to encode the natural numbers. One-hot encoding is one possible unary encoding, where just one bit is “1” and the others are all “0.” The binary encoding needs ⌈log2⁡N⌉ bits, and the unary encoding needs N bits to encode the natural number 0~N.Table 1
Encoding: binary versus unary.
n
Binary
One-hot
0
000
00000001
1
001
00000010
2
010
00000100
3
011
00001000
4
100
00010000
5
101
00100000
6
110
01000000
7
111
10000000Full Adder. A full adder is designed to count the total token numbers to bound the Petri net. As binary and unary encodings are used to represent the token numbers for each place, we present how to design an n-bit binary and unary full adder, respectively.An-bit binary full adder is just combing n single 1-bit binary adders together. The 1-bit binary adder can be described using the following logics. The logics AND, OR, and XOR are represented as ∧, ∨, and ⊕, respectively.(1)S=A⊕B⊕CinCout=A∧B∨Cin∧A⊕BThere are many different ways to design unary adder, but a simplen-bit unary adder is presented as follow:(2)Si=⋀j=0iAj∧Bi-j,0≤i<n.Structural Information. When using unary encoding to represent the token’s number of places, it is important to give this structural information to the SAT solver. Hence, we add some extra logics as a constraint to the AIGER circuits. Figure 2 shows the logics to check if the n-bit vector x is encoded in one-hot. The total number of gates is 3∗n+2.Figure 2
One-hot encoding checking logics.


## 5. Experimental Evaluation

We have implemented the incremental bounded model checking algorithm in a tool named PNPV. PNPV is implemented with C++ and usesminisat as the back-end SAT solver. All input instances are encoded in the MIST format.To measure PNPV’s performance, we compare with TDA [32], which was used to verify parameterized cache coherence protocols. We also compare with the MIST toolkit (https://github.com/pierreganty/mist) with the classical backward [40] and EEC [41] algorithm for WSTS coverability on Petri nets instances.All experiments are performed on a machine, with Intel 2.60 GHz CPU and 16 GB main memory, running CentOS 6.5 in 64-bit. The running time is limited to 600 seconds and memory to 2 GB.


### 5.1. Benchmarks

Memory coherence is very important for both the multicore processors and mobile CPSs. We verify several classical parameterized cache coherence protocols as described in [35]. We collected 12 Petri nets from the MIST repository, where six bounded Petri nets are all safe and six plain Petri nets are all unsafe. Some of those Petri nets are used to model the communication protocols in mobile CPSs.


### 5.2. Evaluation

As shown in Table2, the unary encoding performs about 4~19 times better than binary. By using unary encoding, we can solve 160 processes for Illinois and Firefly protocols, but just 22 and 18 when using binary. For Berkeley, PNPV solves 146 and 18 processes by unary and binary, respectively. German protocol is an industry-like cache coherence protocol, for which 97 and 5 processes are solved by using unary and binary encoding, respectively. The CSMbroad and Dragon protocols both have about 90 processes solved by using the unary encoding but just 9 and 24 processes by using the binary encoding, respectively. The unary encoding is more competitive than binary on all protocols. We identify two reasons for unary’s better performance.Table 2
The maximum process number solved by different encodings. As presented in Section4.3, one-hot encoding is used for unary. Six parameterized protocols are used to test the performance, and the maximum process number is represented in the table. All results are collected by running Algorithm 1.
Protocols
Unary
Binary
Illinois
160
22
Firefly
160
18
Berkeley
146
18
German
97
5
CSMbroad
93
9
Dragon
90
24The first reason is the difference in expressing the transition in FSM. Though there are more variables used to encode the places, the transition relations can be generated by shifting the variables. The logics for transitions are simpler than binary, and the SAT problem is easy to solve.The second reason is the use of the IC3 algorithm. IC3 is an incremental inductive algorithm, which builds the overapproximation from the last SAT results incrementally. The unary encoding is more efficient for learning clauses.Figure3 shows a comparison of the B-bounded model checking algorithm with the incremental bounded model checking algorithm on five parameterized protocols. The incremental bounded model checking algorithm is competitive on all instances, especially for Firefly, Illinois, and Berkeley. The main reason is that theB-bounded algorithm cannot reuse the previous result to prove the current verification problem. Algorithm 1 gives us a good solution with little expenses when adding active literals for the generated FSM.Figure 3
The performance comparison ofB-bounded with incremental bounded model checking algorithm. The superscripts b and inc represent B-bounded model checking algorithm and incremental bounded model checking algorithm, respectively.TDA [32, 33] uses X-abstract and Y-abstract to reduce the state space of parameterized systems and speed up the verification performance. Asynchronous composition is the key part of TDA, but it suffers from higher memory consumption. As shown in Table 3, PNPV performs better than TDA on all parameterized protocols. For Berkeley and Dragon protocols, TDA solves 14 processes, but PNPV solves 146 and 90 processes, respectively. PNPV handles 160 processes for Firefly and Illinois, but just 22 processes are solved by TDA. Table 3 shows that TDA suffers from high memory consumption, as most instances hit the memory limit before hitting the time limit. PNPV is also competitive with respect to speed when comparing with TDA, especially for large process numbers. As the results are all zero when the process number n<10, we present the data from n=10.Table 3
Comparison of running time and memory consumption between PNPV and TDA.n is the number of processes, which is the parameter of the parameterized protocols. Max stands for the maximum number of solved processes. Memory consumption is in MB and running time in seconds.
n
Berkeley
Dragon
Firefly
Illinois
TDA
PNPV
TDA
PNPV
TDA
PNPV
TDA
PNPV
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
10
0.97
16.00
0.62
0.00
1.03
15.50
0.60
0.00
0.59
0.00
0.37
0.00
0.04
0.00
0.49
0.00
11
1.69
46.20
0.66
0.00
0.75
46.20
0.72
0.00
0.61
0.00
0.41
0.00
0.06
0.00
0.54
0.00
12
3.03
130.8
0.71
0.00
3.11
135.1
0.90
6.10
0.64
0.00
0.47
0.00
0.09
0.00
0.60
0.00
13
6.03
416.0
0.78
0.00
8.07
431.4
1.08
6.80
0.69
0.00
0.52
0.00
0.14
0.00
0.67
0.00
14
19.55
1168
0.85
0.00
24.47
1210
0.37
7.10
0.77
0.00
0.60
0.00
0.22
0.00
0.75
0.00
15
Memout
0.94
0.00
Memout
0.64
7.60
0.95
7.90
0.67
0.00
0.42
7.40
0.84
0.00
16
Memout
1.06
0.00
Memout
1.07
8.10
1.24
19.10
0.79
0.00
0.74
18.6
0.96
0.00
17
Memout
0.20
5.00
Memout
0.48
8.70
1.14
40.60
0.89
0.00
1.59
40.60
1.10
5.20
18
Memout
0.37
5.30
Memout
1.13
9.80
1.56
76.20
1.04
5.20
2.25
78.20
0.25
5.20
19
Memout
0.56
5.60
Memout
0.72
10.20
3.68
161.1
0.18
5.40
3.38
161.0
0.42
5.40
20
Memout
0.79
5.90
Memout
1.67
10.90
6.77
311.8
0.39
5.80
6.81
315.4
0.64
5.80
21
Memout
1.04
6.10
Memout
1.52
11.50
13.75
638.2
0.57
5.90
14.33
644.9
0.89
6.00
22
Memout
0.35
6.50
Memout
1.49
12.60
29.61
1249
0.84
6.20
27.28
1224
1.17
6.20
23
Memout
0.70
6.80
Memout
1.98
13.20
Memout
1.09
6.60
Memout
0.49
6.80
Max
14
146
14
90
22
160
22
160MIST is a tool to check safety properties against Petri net-like models. To compare with PNPV, we select the classical backward and EEC algorithms to run 12 Petri net benchmarks. Six out of 12 instances are bounded Petri nets. The total token numbers of the bounded Petri nets are limited. All of the six bounded Petri nets are safe. To test PNPV’s ability of bug finding, six unsafe instances were collected from the MIST toolkit to evaluate the performance.As shown in Table4, PNPV performs better than both backward and EEC algorithms for all unsafe instances. Both in time and memory usage, PNPV is competitive. For six bounded Petri nets, PNPV wins on four out of six instances.Table 4
Comparison of running time and memory consumption for different algorithms on Petri net benchmarks. Memory consumption is in MB, and running time is in seconds.
Problem
PNPV
Backward
EEC
Instance
Time
Mem.
Time
Mem.
Time
Mem.
Safe instances
kanban
7.39
6.60
427.62
54.90
0.83
0.00
lamport
0.42
0.00
0.63
0.00
0.84
0.00
newdekker
0.55
3.30
0.71
0.00
0.85
0.00
newrtp
0.58
0.00
0.72
0.00
0.86
0.00
peterson
0.68
0.00
0.75
0.00
0.86
0.00
read-write
2.31
4.50
0.81
0.00
0.91
0.00
Unsafe instances
kanban
1.05
5.20
459.92
54.90
Timeout
leabasicapproach
0.08
0.00
0.93
0.00
0.08
0.00
pingpong 2
0.10
0.00
0.93
0.00
0.13
0.00
pingpong_wrong
0.13
0.00
0.94
0.00
0.20
0.00
pncsacover
6.22
4.90
Timeout
23.89
8.70
pncsasemiliv
1.06
4.40
1.40
6.00
23.42
8.70


## 5.1. Benchmarks

Memory coherence is very important for both the multicore processors and mobile CPSs. We verify several classical parameterized cache coherence protocols as described in [35]. We collected 12 Petri nets from the MIST repository, where six bounded Petri nets are all safe and six plain Petri nets are all unsafe. Some of those Petri nets are used to model the communication protocols in mobile CPSs.


## 5.2. Evaluation

As shown in Table2, the unary encoding performs about 4~19 times better than binary. By using unary encoding, we can solve 160 processes for Illinois and Firefly protocols, but just 22 and 18 when using binary. For Berkeley, PNPV solves 146 and 18 processes by unary and binary, respectively. German protocol is an industry-like cache coherence protocol, for which 97 and 5 processes are solved by using unary and binary encoding, respectively. The CSMbroad and Dragon protocols both have about 90 processes solved by using the unary encoding but just 9 and 24 processes by using the binary encoding, respectively. The unary encoding is more competitive than binary on all protocols. We identify two reasons for unary’s better performance.Table 2
The maximum process number solved by different encodings. As presented in Section4.3, one-hot encoding is used for unary. Six parameterized protocols are used to test the performance, and the maximum process number is represented in the table. All results are collected by running Algorithm 1.
Protocols
Unary
Binary
Illinois
160
22
Firefly
160
18
Berkeley
146
18
German
97
5
CSMbroad
93
9
Dragon
90
24The first reason is the difference in expressing the transition in FSM. Though there are more variables used to encode the places, the transition relations can be generated by shifting the variables. The logics for transitions are simpler than binary, and the SAT problem is easy to solve.The second reason is the use of the IC3 algorithm. IC3 is an incremental inductive algorithm, which builds the overapproximation from the last SAT results incrementally. The unary encoding is more efficient for learning clauses.Figure3 shows a comparison of the B-bounded model checking algorithm with the incremental bounded model checking algorithm on five parameterized protocols. The incremental bounded model checking algorithm is competitive on all instances, especially for Firefly, Illinois, and Berkeley. The main reason is that theB-bounded algorithm cannot reuse the previous result to prove the current verification problem. Algorithm 1 gives us a good solution with little expenses when adding active literals for the generated FSM.Figure 3
The performance comparison ofB-bounded with incremental bounded model checking algorithm. The superscripts b and inc represent B-bounded model checking algorithm and incremental bounded model checking algorithm, respectively.TDA [32, 33] uses X-abstract and Y-abstract to reduce the state space of parameterized systems and speed up the verification performance. Asynchronous composition is the key part of TDA, but it suffers from higher memory consumption. As shown in Table 3, PNPV performs better than TDA on all parameterized protocols. For Berkeley and Dragon protocols, TDA solves 14 processes, but PNPV solves 146 and 90 processes, respectively. PNPV handles 160 processes for Firefly and Illinois, but just 22 processes are solved by TDA. Table 3 shows that TDA suffers from high memory consumption, as most instances hit the memory limit before hitting the time limit. PNPV is also competitive with respect to speed when comparing with TDA, especially for large process numbers. As the results are all zero when the process number n<10, we present the data from n=10.Table 3
Comparison of running time and memory consumption between PNPV and TDA.n is the number of processes, which is the parameter of the parameterized protocols. Max stands for the maximum number of solved processes. Memory consumption is in MB and running time in seconds.
n
Berkeley
Dragon
Firefly
Illinois
TDA
PNPV
TDA
PNPV
TDA
PNPV
TDA
PNPV
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
Time
Mem.
10
0.97
16.00
0.62
0.00
1.03
15.50
0.60
0.00
0.59
0.00
0.37
0.00
0.04
0.00
0.49
0.00
11
1.69
46.20
0.66
0.00
0.75
46.20
0.72
0.00
0.61
0.00
0.41
0.00
0.06
0.00
0.54
0.00
12
3.03
130.8
0.71
0.00
3.11
135.1
0.90
6.10
0.64
0.00
0.47
0.00
0.09
0.00
0.60
0.00
13
6.03
416.0
0.78
0.00
8.07
431.4
1.08
6.80
0.69
0.00
0.52
0.00
0.14
0.00
0.67
0.00
14
19.55
1168
0.85
0.00
24.47
1210
0.37
7.10
0.77
0.00
0.60
0.00
0.22
0.00
0.75
0.00
15
Memout
0.94
0.00
Memout
0.64
7.60
0.95
7.90
0.67
0.00
0.42
7.40
0.84
0.00
16
Memout
1.06
0.00
Memout
1.07
8.10
1.24
19.10
0.79
0.00
0.74
18.6
0.96
0.00
17
Memout
0.20
5.00
Memout
0.48
8.70
1.14
40.60
0.89
0.00
1.59
40.60
1.10
5.20
18
Memout
0.37
5.30
Memout
1.13
9.80
1.56
76.20
1.04
5.20
2.25
78.20
0.25
5.20
19
Memout
0.56
5.60
Memout
0.72
10.20
3.68
161.1
0.18
5.40
3.38
161.0
0.42
5.40
20
Memout
0.79
5.90
Memout
1.67
10.90
6.77
311.8
0.39
5.80
6.81
315.4
0.64
5.80
21
Memout
1.04
6.10
Memout
1.52
11.50
13.75
638.2
0.57
5.90
14.33
644.9
0.89
6.00
22
Memout
0.35
6.50
Memout
1.49
12.60
29.61
1249
0.84
6.20
27.28
1224
1.17
6.20
23
Memout
0.70
6.80
Memout
1.98
13.20
Memout
1.09
6.60
Memout
0.49
6.80
Max
14
146
14
90
22
160
22
160MIST is a tool to check safety properties against Petri net-like models. To compare with PNPV, we select the classical backward and EEC algorithms to run 12 Petri net benchmarks. Six out of 12 instances are bounded Petri nets. The total token numbers of the bounded Petri nets are limited. All of the six bounded Petri nets are safe. To test PNPV’s ability of bug finding, six unsafe instances were collected from the MIST toolkit to evaluate the performance.As shown in Table4, PNPV performs better than both backward and EEC algorithms for all unsafe instances. Both in time and memory usage, PNPV is competitive. For six bounded Petri nets, PNPV wins on four out of six instances.Table 4
Comparison of running time and memory consumption for different algorithms on Petri net benchmarks. Memory consumption is in MB, and running time is in seconds.
Problem
PNPV
Backward
EEC
Instance
Time
Mem.
Time
Mem.
Time
Mem.
Safe instances
kanban
7.39
6.60
427.62
54.90
0.83
0.00
lamport
0.42
0.00
0.63
0.00
0.84
0.00
newdekker
0.55
3.30
0.71
0.00
0.85
0.00
newrtp
0.58
0.00
0.72
0.00
0.86
0.00
peterson
0.68
0.00
0.75
0.00
0.86
0.00
read-write
2.31
4.50
0.81
0.00
0.91
0.00
Unsafe instances
kanban
1.05
5.20
459.92
54.90
Timeout
leabasicapproach
0.08
0.00
0.93
0.00
0.08
0.00
pingpong 2
0.10
0.00
0.93
0.00
0.13
0.00
pingpong_wrong
0.13
0.00
0.94
0.00
0.20
0.00
pncsacover
6.22
4.90
Timeout
23.89
8.70
pncsasemiliv
1.06
4.40
1.40
6.00
23.42
8.70


## 6. Conclusion and Future Works

We introduced an incremental bounded model checking algorithm to verify the safety properties of parameterized protocols in mobile CPS. By using counter abstraction, the protocol is modeled as a Petri net. Then the state-of-the-art SAT-based model checking algorithm is used to verify the safety properties. The algorithm can be used to verify parameterized systems, including cache coherence protocols, mutual exclusion communication protocols, and common concurrency primitives in mobile CPSs. The results show that our new approach can greatly scale the verification capabilities compared favorably against several recently published approaches. Due to using IC3 as the back-end model checking algorithm, our method is significant for its lower memory consumption.There are two directions to extend the current work in the future. The first one is to study the property to be verified. Liveness would be an interesting direction, as the liveness property can be converted into safety. Security problems and run time verification would also be a good direction in the future. The second one is to model more complex systems. The ideas we have presented are naturally applicable to other concurrency systems modeled by Petri net or its extension. It is natural to shift SAT solver to SMT solver, and it would be a good way to improve the scalability.



---

*Source: 5731678-2017-05-10.xml*