Unified Bounded Model Checking for MSVL

Abstract

This paper presents Unified Bounded Model Checking (UBMC) for the verification of an infinite state system described with Modeling, Simulation and Verification Language (MSVL) which is an executable subset of Projection Temporal Logic (PTL). The desired property is specified by a Propositional PTL (PPTL) formula. We present the bounded semantics of PPTL and the approach to implementing UBMC. A Bounded Labeled Normal Form Graph (BLNFG) is constructed on the fly and a counterexample of minimal length is produced to ease the interpretation and understanding for debugging purposes. Finally, a resource allocation algorithm is presented as an example to illustrate how the proposed approach works.

This research is supported by the NSFC Grant No. 61133001, 61272117, 61322202, 61420106004, and 91418201.

1 Introduction

Techniques for automatic formal verification of finite state transition systems have been studied in recent years. Compared to other formal verification techniques (e.g. theorem proving), model checking [1, 2] is an automatical approach. Model checking has been widely used in many fields such as verification of hardware, software and communication protocols. In model checking, the system to be verified is modeled as a finite state machine, and the specification is formalized by a temporal logic formula.

For a system in practice, the number of states in it can be very large and the explicit traversal of the state space becomes infeasible. To fight with this problem, several approaches, such as Symbolic Model Checking (SMC) [3], Abstract Model Checking (AMC) [4], and Compositional Model Checking [5], etc. have been proposed with success. The combination of symbolic model checking with BDDs [6, 7] pushed the barrier to systems with $10^{20}$ states and more later [3]. But the bottleneck of SMC is the amount of memory that is required for storing and manipulating BDDs. The boolean functions required to represent the set of states can grow exponentially. Bounded model checking (BMC) is an important progress in formal verification after SMC [8]. The basic idea in BMC is to search for a counterexample in executions whose length is bounded by some integer $k$. If the property is not satisfied, an error is found. Otherwise, we cannot tell whether the system satisfies the property or not. In this case, we can consider to increase $k$, and then perform the process of BMC again. BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures do not suffer from the state space explosion problem of BDD-based methods. Modern SAT solvers can handle propositional satisfiability problems with hundreds of thousands of variables or more. Tools supporting BMC are NuSMV2 [9], bounded model checker developed by CMU [10], Thunder of Intel [11], and so on.

With model checking and bounded model checking, the mostly used temporal logics are LTL [12], CTL [1], and their variations. However, expressiveness of both LTL and CTL is not powerful enough. There are at least two types of properties in practice which cannot (or with difficulty to) be specified by LTL and CTL: (1) time related properties such as “a property $P$ holds after the $100^{th}$ time unit and before the $200^{th}$ time unit”; (2) periodically repeated of property $P$. The expressiveness of Propositional Projection Temporal Logic (PPTL) [13] is full regular [14] which allows us to verify full regular properties and time related properties of systems in a convenient way.

In recent years, the verification of infinite state systems has attained increasing interest. The main limitation of model checking is that it is restricted to (essentially) finite-state systems. In general, the model checking problem is undecidable for infinite state systems, and hence, it may happen that the verification process does not terminate. In the verification of an infinite state system, theorem proving [15] is a powerful technique. Predicate abstraction has been introduced as a technique for reduction of infinite state systems to finite one in the work of Graf and Saidi [16]. Verification by abstraction can be applied to infinite state systems as shown in [17–19]. Another way to deal with the difficulty of verification is the method of compositional verification that uses the combination of temporal case splitting and data type reductions to reduce types of infinite or unbounded range to small finite types, and arrays of infinite or unbounded size to small fixed-size arrays [20, 21]. In bounded model checking of infinite state systems [22], three-valued logic is employed in order to explicitly forward uncertain information in the case a proof cannot be established due to insufficient bounds.

Modeling, Simulation and Verification Language (MSVL) is a subset of Projection Temporal Logic (PTL) [13, 23] with framing techniques [24]. It can be used for the purpose of modeling, simulation and verification of software and hardware systems. For the verification of a finite system by MSVL, a method named Unified Model Checking has been presented in [25]. With this method, a system is first modeled as $p$ in MSVL. Thus, $p$ is a non-deterministic program of MSVL and also a formula of PTL. Second, the property we want to check is specified by a formula $\phi$ in PPTL. To check whether or not $p$ satisfies $\phi$ amounts to proving $\models p \rightarrow \phi$. It turns out to prove $\not \models p\wedge \lnot \phi$. Thus, for finite state programs in MSVL, we can translate the model checking problem into a satisfiability problem in PPTL since finite state programs in MSVL are equivalent to PPTL formulas. To check the satisfiability of $p \wedge \lnot \phi$, Labeled Normal Form Graph (LNFG) of $p \wedge \lnot \phi$ can be constructed. But for an infinite state transition system, the path in the LNFG may be a straight infinite line and we cannot get the result that whether the system satisfies the given property forever.

Given an infinite system $p$ in MSVL, a property of the system in terms of a PPTL formula $\phi$, and a user supplied upper bound $k$, we present an approach named Unified Bounded Model Checking (UBMC) which combines bounded model checking and unified model checking approaches. In order to do this, bounded semantics of PPTL is presented. Further, the procedure of UBMC can be described as a process to construct the Bounded Labeled Normal Form Graph (BLNFG) of $p\wedge \lnot \phi$ on the fly. BLNFG is constructed progressively as the current bound increases. If a finite or an infinite counterexample is found at a given bound that is less than the upper bound, the construction of the BLNFG stops and the counterexample is output. When there is no new node to be dealt with and no counterexample is found, the construction of BLNFG terminates and the result is given that the property is valid. If the current bound is increasing until the upper bound with no counterexamples found, it cannot be determined whether the system satisfies the property or not. At this time, we can increase the upper bound and construct the BLNFG of $p\wedge \lnot \phi$ again.

The main advantages of our technique are the follows. First, our method can partially verify an infinite system described by MSVL. We can give the result that whether the property is valid in bound $k$. Second, our method can find counterexamples relatively quicker. This is due to the depth first nature in the construction of our BLNFG. Finding counterexamples is arguably the most important feature of model checking. Third, it finds a counterexample of minimal length. This feature helps users to understand a counterexample more easily.

This paper is organized as follows. In the next section, as a property specification language, PPTL formulas are presented. Then the language MSVL used for the description of an infinite system is formalized. In Sect. 3, the bounded semantics of PPTL formulas is given. Next, the method for constructing a BLNFG is formalized in detail. A resource allocation algorithm is presented to illustrate how our approach works in Sect. 5. Finally, conclusion is drawn in Sect. 6.

2 Preliminaries

2.1 Propositional Projection Temporal Logic

Let $Prop$ be a countable set of atomic propositions. A formula $P$ of PPTL is given by the following grammar:

$$\begin{aligned} P:: = p\ |\ \bigcirc P\ |\ \lnot P\ |\ {P_1} \vee {P_2}\ |\ ({P_1}, \cdots {P_m})\ prj\ P \end{aligned}$$

where $p \in Prop$, $P_1,\cdots ,P_m$ and $P$ are all well-formed PPTL formulas. $\bigcirc \ (next)$ and $prj \ (projection)$ are basic temporal operators.

A mapping from $Prop$ to $B=\{true, false\}$ is used to define a state $s$, $s: Prop\rightarrow B$. $s[p]$ denotes the valuation of $p$ at the state $s$. An interval $\sigma$ is a non-empty sequence of states. The length of $\sigma$, $| \sigma |$, is the number of states minus 1 if $\sigma$ is finite, and $\omega$ otherwise. The set of non-negative integers $N_0$ with {$\omega$}, $N_{\omega }=N_0 \cup \{ \omega \}$ is used for both finite and infinite intervals. The relational operators, $=, <, \le$, is extended to $N_{\omega }$ by considering $\omega = \omega$, and for all $i\in N_0, i<\omega$. Moreover, the relation symbol $\preceq$ is defined as $\le - {(\omega , \omega )}$.

In an interpretation $\mathcal {I} =(\sigma ,i,j)$, $\sigma$ is an interval, $i$ an integer, and $j$ an integer or $\omega$ such that $i\preceq j\le |\sigma |$. If formula $P$ is interpreted and satisfied over a subinterval $<s_i,\cdots , s_j >$ of $\sigma$ with the current state being $s_i$, it is denoted by the notation $(\sigma ,i, j)\models P$. The satisfaction relation $(\models )$ is inductively defined as follows:

$$ \begin{array}{lll} I-prop &{} \mathcal {I}\models &{}p \text{ iff } s_i[p]=true, \text{ and } p\in Prop \text{ is } \text{ an } \text{ proposition } \\ I-not &{} \mathcal {I}\models &{}\lnot P \text{ iff } \mathcal {I}\not \models P \\ I-or &{} \mathcal {I}\models &{}P\vee Q \text{ iff } \mathcal {I}\models P \text{ or } \mathcal {I}\models Q \\ I-next &{} \mathcal {I}\models &{}\bigcirc P \text{ iff } i<j \text{ and } (\sigma ,i+1,j)\models P\\ I-prj &{} \mathcal {I}\models &{} (P_1, \cdots , P_m)~prj~P, \text{ if } \text{ there } \text{ exist } \text{ inte } \text{ gers } r_0\le r_1\le \cdots \le r_m\le j \\ ~&{}~&{} \text{ such } \text{ that } (\sigma ,r_0,r_1)\models P_1,~(\sigma ,r_{l-1},r_l)\models P_l, 1<l\le m, \text{ and } (\sigma ',0,|\sigma '|)\models Q \\ ~&{}~&{} \text{ for } \text{ one } \text{ of } \text{ the } \text{ following } \sigma '{:}\\ ~&{}~&{}(a)~r_m<j \text{ and }\sigma '=\sigma \downarrow (r_0, \cdots , r_m)\cdot \sigma _{(r_m+1,\cdots ,j)}, \text{ or } \\ ~&{}~&{}(b)~r_m=j \text{ and } \sigma '=\sigma \downarrow (r_0, \cdots , r_h) \text{ for } \text{ some } 0\le h\le m. \end{array} $$

where $P$, $P_1,\cdots ,P_m$ and $Q$ are PPTL formulas.

A formula $P$ is satisfied by an interval $\sigma$, denoted by $\sigma \models P$, if $(\sigma , 0, |\sigma |)\models P$. A formula $P$ is called satisfiable if $\sigma \models P$ for some $\sigma$. A formula $P$ is valid, denoted by $\models P$, if $\sigma \models P$ for all $\sigma$.

For any PPTL formula $Q$, it can be rewritten into its normal form [26]:

$${NF(Q) \equiv \bigvee \limits _{j=0}^{n_0}(Q_{ej} \wedge empty)\vee \bigvee \limits _{i=0}^n(Q_{ci}\wedge \bigcirc Q_{fi})}$$

where $Q_{ej}$ and $Q_{ci}$ are conjunctions of atomic propositions (or their negations) in $Q_p$ which is the set of atomic propositions appearing in the PPTL formula $Q$, and $Q_{fi}$ is an arbitrary PPTL formula.

Fig. 1.

LNFG of formula $\lnot (true;\lnot \bigcirc q) \wedge (p \vee \bigcirc (p;q))$

For a PPTL formula $Q$, its corresponding LNFG can be constructed, which explicitly illustrates models of the formula. Here, an example is given to show the LNFG of a PPTL formula intuitively and the formal definition can be found in [27].

Example 1

LNFG of formula $\lnot (true;\lnot \bigcirc q) \wedge (p \vee \bigcirc (p;q))$ is shown in Fig. 1.

In the LNFG of a formula as shown in Fig.1, each node is specified by a PPTL formula, while each edge is a directed arc labeled with a state formula. The extra propositions $l_k$ are employed to mark the infinite paths in the LNFG which are not the models of the PPTL formula.

2.2 Modeling, Simulation and Verification Language

MSVL is a subset of Projection Temporal Logic [13, 23] with framing technique [24]. Based on the language, we have developed a model checking tool named MSV which works in three modes: modeling, simulation and verification.

The arithmetic expression e and boolean expression b of MSVL are inductively defined as follows:

$$ \begin{array}{llll} e&{}::=&{}\ n\ | \ x\ | \ \bigcirc x\ | \ \bigcirc \!\!\!\!\!\!\!{\small {-}} \, x\ |\ e_0\ op\ e_1\ (op::= +|-|*|\backslash |mod)\\ b&{}::=&{}\ true\ |\ false \ |\ e_0 = e_1 \ | \ e_0 < e_1 \ |\ \lnot b\ | \ b_0\ \wedge \ b_1\\ \end{array} $$

where $n$ is an integer and $x$ a variable. The elementary statements in MSVL are defined as follows. The meanings of all statements in MSVL are given in [13].

Termination: $empty$     State Assignment: $x<==e$     Assignment: $x:=e$

State Frame: $lbf(x)$        Interval Frame: $frame(x)$        Conjunction: $p\wedge q$

Selection: $p \vee q$           Next: $\bigcirc p$             Always: $\Box p$       Sequence: $p;q$

Conditional: $if\ b\ then\ p\ else\ q$ $\mathop = \limits ^\mathrm{def} (b \rightarrow p) \wedge (\lnot b \rightarrow q)$

While: $while\ b\ do\ p\$ $\mathop = \limits ^{\mathrm{{def}}} (p \wedge b)^{*} \wedge \Box (empty \rightarrow \lnot b)$

where $x$ denotes a variable, $e$ stands for an arbitrary arithmetic expression, $b$ denotes a boolean expression, and $p$, $q$ stand for programs of MSVL.

Any MSVL program $p$ can be rewritten into its normal form [13, 24]. According to normal form, we can construct an LNFG $G=(CL(p), EL(p), v_0,\mathbb {L}=\{\mathbb {L}_1,\ldots ,\mathbb {L}_m\})$ to model an infinite state MSVL program $p$. Each node is specified by a program in MSVL, while each edge is a directed arc labeled with a state formula $p_e$ from node $q$ to node $r$ and identified by a triple, $(q,p_e,r)$.

Note that the number of nodes is finite only when the range of values of the variables in the program is limited to a finite set. When the range of variables is infinite, we cannot construct a finite LNFG of the program. For example, in the program $frame(i) \ and \ (int \ i<==0 \ and \ skip; \ while(true) \{ (i:=i+1)\})$, the value of $i$ is increasing and a finite LNFG of the program cannot be constructed always. In the LNFG of an infinite state MSVL program, there exist three kinds of paths: finite paths, loop paths and infinite paths with infinite states.

3 Bounded Semantics for PPTL

The basic idea of bounded model checking, as explained before, is to consider only a finite prefix of a path that may be a witness to the desired property. We restrict the length of the prefix by some bound $k$. In practice, we progressively increase the bound, looking for witnesses in longer and longer traces.

A crucial observation is that, though the prefix of a path is finite, it still might represent an infinite path if there is a back loop from the last state of the prefix to any of the previous states as in Fig. 2. If there is no such loop, as in Fig. 3, the prefix does not say anything about the behavior of the path beyond state $s_k$.

Fig. 2.

$\sigma$ is a $(k,l)$-loop

Fig. 3.

$\sigma$ is a finite interval

Definition 1

((k,l)-loop). For $l,k\in N_0$ and $l \le k$, if there is a transition from $s_k$ to $s_l$ in $\sigma$ i.e. $\sigma =(s_0,\cdots ,s_{l-1}) \cdot (s_l,\cdots ,s_k)^{\omega }$, we call interval $\sigma$ a (k, l)-loop, k-loop for short.

Obviously, if $\sigma$ is an infinite interval with a loop, it must be a $k$-loop for some $k\in N_0$. We will use the notion of $k$-loop in order to define the bounded semantics of PPTL. The bounded semantics is an approximation to the unbounded semantics, which will allow us to define the bounded model checking problem. Since each PPTL formula can be transformed into an equivalent formula in NF, we do not need to deal with all types of PPTL formulas in the bounded semantics.

In the bounded semantics, we only consider a finite prefix of a path. In particular, we only use the first $k + 1$ states $(s_0,\ldots ,s_k)$ of a path to determine the validity of a formula along the path. If a path is a $k$-loop then we simply maintain the original semantics of atomic propositions, $\lnot$, $\vee$, and $\bigcirc$ operators, because all the information about this infinite path is contained in the prefix of length $k$. Since $empty \equiv \lnot \bigcirc true$ and $more \equiv \bigcirc true$, the bounded semantics of $empty$ and $more$ can be deduced by the bounded semantics of $\lnot$ and $\bigcirc$. In fact, the formula $empty$ cannot be satisfied over an infinite interval, while $more$ is satisfied all the time in an infinite interval.

Definition 2

(Bounded Semantics for a Loop). Let $k \in N_0$ and $\sigma$ be a $k$-loop interval, a PPTL formula $f$ is valid along $\sigma$ with bound $k$ (denoted by $\sigma \models _k f$) iff $\sigma \models f$.

We now consider the case where $\sigma$ is not a $k$-loop. We use the notation $(\sigma ,i) \models _k f$ $(0\le i \le k \le |\sigma |)$ to represent that formula $f$ is interpreted and satisfied over the subinterval $<s_i,\cdots ,s_k>$ of $\sigma$ with the current state being $s_i$. $(\sigma ,0) \models _k f$ is denoted by $\sigma \models _k f$.

In the bounded semantics without a loop, we only consider formulas constructed from atomic propositions and negations of atomic propositions with $\vee$, $\wedge$, and $\bigcirc$ operators as well as $empty$ and $more$.

Definition 3

(Bounded Semantics without a Loop). Let $k \in N_0$ and $\sigma$ be an interval that is not a $k$-loop. The bounded satisfaction relation $\models _k$ is defined as follows:

$$ \begin{array}{lll} (\sigma ,i)\models _k p ~&{} \text{ iff } &{}~ s_i[p]=true \text{ if } p\in Prop \text{ is } \text{ an } \text{ atomic } \text{ proposition }\\ (\sigma ,i)\models _k \lnot p ~&{} \text{ iff } &{}~ s_i[p]=false \text{ if } p\in Prop \text{ is } \text{ an } \text{ atomic } \text{ proposition }\\ (\sigma ,i)\models _k P_1\vee P_2 ~&{}\text{ iff } &{}~ (\sigma ,i)\models _k P_1 \text{ or } (\sigma ,i)\models _k P_2 \\ (\sigma ,i)\models _k P_1\wedge P_2 ~&{}\text{ iff } &{}~ (\sigma ,i)\models _k P_1 \text{ and } (\sigma ,i)\models _k P_2 \\ (\sigma ,i)\models _k \bigcirc P ~&{} \text{ iff } &{}~ i+1\le k \text{ and } (\sigma ,i+1)\models _k P \\ (\sigma ,i)\models _k empty ~&{}\text{ iff } &{}~ i=|\sigma | \\ (\sigma ,i)\models _k more ~&{} \text{ iff } &{}~ i<|\sigma | \end{array} $$

Lemma 1

Let $k\in N_0$, $f$ be a PPTL formula, and $\sigma$ a finite interval. We have $\sigma \models _k f \Rightarrow \sigma \models f$.

Proof: To prove $Lemma$ 1, we first prove a stronger conclusion given below:

$$\begin{aligned} (\sigma , i)\models _k f \Rightarrow (\sigma , i, |\sigma |)\models f ~~( 0\le i\le k) \end{aligned}$$

$Lemma$ 1 can be concluded by setting $i=0$. We prove the above conclusion by induction on the structure of formula $f$:

Base case:

$f\equiv p\in Prop: (\sigma , i)\models _k p \Rightarrow s_i[p]=true \Rightarrow (\sigma , i, |\sigma |)\models p$

$f\equiv \lnot p\in Prop: (\sigma , i)\models _k \lnot p \Rightarrow s_i[p]=false \Rightarrow (\sigma , i, |\sigma |)\not \models p \Rightarrow (\sigma , i, |\sigma |)\models \lnot p$

$f\equiv empty:(\sigma , i)\models _k empty \Rightarrow i=|\sigma | \Rightarrow (\sigma , i, |\sigma |)\models empty$

Inductive cases: Suppose for any PPTL formula $f$, $(\sigma , i)\models _k f \Rightarrow {(\sigma , i, |\sigma |)\models f}$.

• 1. By hypothesis, when $i < k \le |\sigma |$, we have $(\sigma , i+1)\models _k f \Rightarrow (\sigma , i+1,|\sigma |)\models f$. By the definitions of semantics, $(\sigma , i+1)\models _k f \text{ iff } (\sigma , i)\models _k \bigcirc f$ and $(\sigma , i+1,|\sigma |)\models f \text{ iff } (\sigma , i,|\sigma |)\models \bigcirc f$, so we can get $(\sigma , i)\models _k \bigcirc f \Rightarrow (\sigma , i,|\sigma |)\models \bigcirc f$. When $i=k$, $(\sigma , i+1)\models _k f$ is $false$. Because $false \Rightarrow (\sigma , i,|\sigma |)\models \bigcirc f$, we can get $(\sigma , i)\models _k \bigcirc f \Rightarrow (\sigma , i,|\sigma |)\models \bigcirc f$.

• 2. By hypothesis, we have $(\sigma ,i)\models _k P_1$ $\Rightarrow$ $(\sigma ,i,|\sigma |)\models P_1$ and $(\sigma ,i)\models _k P_2$ $\Rightarrow$ $(\sigma ,i,|\sigma |)\models P_2$. By the definitions of bounded semantics, we can easily get $(\sigma ,i)\models _k P_1\,\vee \, P_2 \Rightarrow (\sigma ,i,|\sigma |)\models P_1\,\vee \, P_2$. Similarly, $(\sigma ,i)\models _k P_1\wedge P_2 \Rightarrow (\sigma ,i,|\sigma |)\models P_1\,\wedge \,P_2$.

Note that we do not need to deal with $more$ in the above inductive cases since $more \equiv \bigcirc true$.

Lemma 2

Let $f$ be a PPTL formula and $\sigma$ a finite interval. Then $\sigma \models f \Rightarrow \exists k, k \in N_0, \sigma \models _k f$.

Proof: Since $\sigma$ is a finite interval, so $|\sigma |\in N_0$.

$$ \begin{array}{lll} &{} \sigma \models f &{}\Rightarrow (\sigma ,0,|\sigma |) \models f\\ &{} &{}\Rightarrow (\sigma ,0,k) \models f \wedge k=|\sigma |\\ &{} &{}\Rightarrow \exists k, k\ge 0, (\sigma ,0) \models _k f\\ &{} &{}\Rightarrow \exists k, k\ge 0, \sigma \models _k f \end{array} $$

4 Unified Bounded Model Checking of MSVL

In the Unified Model Checking implemented in [25], LNFG of $p \wedge \lnot \phi$ is constructed to check whether a finite state MSVL program $p$ satisfies a PPTL formula $\phi$. According to [27], finite and infinite models of $p \wedge \lnot \phi$ are precisely characterized by the paths which satisfy certain conditions in the LNFG. For a PPTL formula $Q$, an interval $\sigma _{\pi }$ can be defined for a given path $\pi$ in the LNFG of formula $Q$ and given a model $\sigma$ of formula $Q$ , $\sigma \models Q$, a path $\pi _{\sigma }$ can be constructed according to the transition rules [27].

In the previous section, we defined the bounded semantics of PPTL. According to it, a BLNFG can be constructed to describe the model of $p \wedge \lnot \phi$ in bound $k$.

Definition 4

(Bounded Labeled Normal Form Graph, BLNFG). For a MSVL program $p$, a PPTL formula $\phi$, and $k \in N_0$, its BLNFG is a tuple $G=(CL(p \wedge \lnot \phi ), EL(p \wedge \lnot \phi ), v_0,\mathbb {L}=\{\mathbb {L}_1,\ldots ,\mathbb {L}_m\},\mathbb {C}=\{\mathbb {C}_1,\ldots ,\mathbb {C}_k\})$, where $CL(p \wedge \lnot \phi ), EL(p \wedge \lnot \phi ), V_0$ and $\mathbb {L}$ are identical to the ones defined in [27] and each $\mathbb {C}_i \subseteq CL(p \wedge \lnot \phi ), 0 \le i \le k$, is the set of nodes with $c_q=i$, where $c_q$ represents the depth of a node $q$.

Since the set $CL(p \wedge \lnot \phi )$ of nodes and the set $EL(p \wedge \lnot \phi )$ of edges are inductively produced by repeatedly rewriting the new created nodes into their normal forms, the BLNFG can be constructed progressively with the current bound increasing until a user supplied upper bound $k$. When constructing BLNFGs by normal form reductions, for any chop formula $P;Q$, we equivalently rewrite it by $P \wedge fin(l_k);Q$ as implemented in [27]. For convenience, we use inf $(\pi )$ to denote the set of nodes which infinitely often occur in the infinite path $\pi$.

By conclusions in [27], we can get the Corollaries 1 and 2 respectively as follows.

Corollary 1

If $\pi$ is a finite or an infinite path with inf $(\pi ) \nsubseteq \mathbb {L}_i$ for all $1\le i \le m$ and $c_q \le k \ (k \in N_0)$ for all nodes $q$ on $\pi$ in the BLNFG of formula $p \wedge \lnot \phi$, then the interval obtained from the path $\sigma _{\pi } \models _k p \wedge \lnot \phi$.

Corollary 2

For a finite or an infinite interval $\sigma$, if $\sigma \models _k p \wedge \lnot \phi$, then $\pi _{\sigma }$ translated from $\sigma$ with inf $(\pi _{\sigma }) \nsubseteq \mathbb {L}_i$ for all $1\le i \le m$ and $c_q \le k$ for all nodes $q$ on $\pi _{\sigma }$ can be found in the BLNFG of formula $p \wedge \lnot \phi$.

Corollaries 1 and 2 tell us that a finite or an infinite interval $\sigma \models _k p \wedge \lnot \phi$ iff there exists a corresponding finite or infinite path satisfying certain conditions in the BLNFG of formula $p \wedge \lnot \phi$ in bound $k$.

Because a MSVL program $p$ does not satisfy a PPTL formula $\phi$ iff $p \wedge \lnot \phi$ is satisfiable, then we can get the following corollary which is important in our unified bounded model checking.

Corollary 3

In the LNFG of an infinite system $p$ in MSVL, finite paths precisely characterize finite models of $p$; loop paths with inf $(\pi ) \nsubseteq \mathbb {L}_i$ for all $1\le i \le ~ m$, precisely characterize loop models of $p$.

According to Corollary 3, our bounded model checking approach can be deduced to the construction of the BLNFG of $p \wedge \lnot \phi$. In the on-the-fly construction of $p\wedge \lnot \phi$, $i$ is the current bound which stops increasing once a counterexample is found or reaches the upper bound. Initially, we create the root node $p\wedge \lnot \phi$ and set $c_{p\wedge \lnot \phi }$ to 0.

Fig. 4.

The construction of the BLNFG for $p \wedge \lnot \phi$

For a given bound $i$, nodes whose depth equals $i$ are dealt with. In order to retain consistency, we use $p\wedge \lnot \phi$ to represent the node that will be dealt with. For a node $p\wedge \lnot \phi$, $p$ and $\lnot \phi$ are rewritten into their normal forms respectively. The function $NF()$ defined in [26] is called to produce normal form of a PPTL formula or MSVL program. Then we can get the conjunction of these two normal forms. The first part of the conjunction is a disjunction. A finite path ended by the empty node is found once one disjunct can be satisfied. At this time, the construction of the BLNFG terminates and a finite counterexample is output. Because the depth of nodes that are dealt with is increasing progressively, our process produces counterexamples of minimal length, which eases the understanding for debugging purposes. If no counterexample is found by checking the first part, the second part of the conjunction will be dealt with. For every disjunct, a new node will be generated if the present state can be satisfied. If the node $p_{fj}\wedge \lnot \phi _{fs}$ does not exist, a new node $p_{fj}\wedge \lnot \phi _{fs}$ whose depth is $i+1$ is generated. Otherwise, a loop will be generated. If inf $(\pi ) \nsubseteq \mathbb {L}_i$ for all $1\le i \le m$, the infinite path is output as a counterexample and the construction of BLNFG terminates. If not, this infinite interval is not a model of $p \wedge \lnot \phi$ and is not taken into account. At this time, we will check whether there exist other nodes whose depth is equal to $i$. If these nodes exist, they will be dealt with by the same process above. Those new generated nodes whose depth is equal to $i+1$ will not be dealt with immediately. When the current bound increases to $i+1$, $p_{fj}\wedge \lnot \phi _{fs}$ will be considered.

In case that all nodes whose depth is $i$ have been dealt with and no counterexample has been found, the current bound $i$ will increase. If there is no node to be dealt with at this time, it means that the whole LNFG of $p\wedge \lnot \phi$ has been constructed. Because no valid path exists in the LNFG, we can get the result that the property $\phi$ is valid. If the value of $i$ is still less than the upper bound $k$, the nodes whose depth equals $i$ will be dealt with by the same process above. If the value of $i$ is larger than the upper bound $k$, the process has to stop and it cannot be determined whether the system satisfies the property or not. The construction of the BLNFG for $p \wedge \lnot \phi$ is depicted in Fig. 4.

Based on our UBMC algorithm, the model checker acting as a module in the MSV toolkit [25] has been developed. Under the bounded verification mode, a finite or an infinite system model is described by a MSVL program and the property is specified by a PPTL formula. A upper bound can be set by the user, otherwise it will be the default value.

5 A Case Study: Verification of Resource Allocation Algorithm

Banker’s algorithm [28] is a resource allocation and deadlock avoidance algorithm developed by Dijkstra. It tests for safety by simulating the allocation of predetermined maximum possible amounts of all resources. The algorithm tests for possible deadlock conditions for all other pending activities before deciding whether allocation is permitted.

Fig. 5.

The verification result of the resource allocation algorithm

The algorithm is originally developed in the design process of operating systems. When a new process enters a system, it must declare the maximum number of each resource type that it may ever claim. When a process gets all its requested resources, it must return them in a finite time interval. Many variations of Banker’s algorithm have been applied in cloud computing where different computing tasks may be assigned to different platforms. Because resources available are usually limited on a given platform, it becomes necessary to check whether the tasks to be executed are schedulable.

We describe a variation of the resource allocation algorithm by a MSVL program where it is assumed that five tasks need to be scheduled every time and there exist four types of resources to be allocated. An array $maxres$ is used to indicate the number of resources available of each type. A $5 \times 4$ matrix $maxclaim$ defines the maximum demand of each task and another $5 \times 4$ matrix $curr$ defines the number of resources which are already allocated to each task. In the program, the platform keeps running through a nonterminal loop and the maximum demand of each task changes among three cases randomly. A boolean variable $fail$ is used to represent whether the tasks are schedulable in each case and $order$ is an array used to record every task’s execution order.

Assume that we want to check whether or not the tasks are schedulable in each case and the third task is always executed after the second one. The property can be specified by $\Box (p \wedge q)$ in PPTL where $p$ is defined as $fail=0$ and $q$ is defined as $order[1]<order[2]$. The upper bounded length is set to 100. Then we can verify the model with the bounded model checker. The verification result is shown in Fig. 5.

The counterexample is found when the bound increases to 89. By analysing the counterexample, we find that the resources available are too limited to schedule these five tasks. When the variable $maxclaim$=[[4, 2, 1, 4], [2, 2, 5, 2], [5, 1, 3, 5], [3 ,5 ,3 ,0], [3 ,2 ,3 ,3]], the first and the fourth types of resources are not enough. The program is verified again after we add one resource to the first and the fourth types respectively. Then we can get the result that the given property is valid for the modified program.

6 Conclusion

In this paper, we have proposed an approach named UBMC, which combines bounded model checking with unified model checking for verifying infinite state programs in MSVL. In our approach, a BLNFG is constructed on the fly to find whether there exist counterexamples in the given bound. This new technique produces counterexamples of minimal length and speeds up the verification. We also use a resource allocation example to show our approach. To examine our method, several case studies with larger examples are required in the near future. Moreover, lots of efforts are needed to improve our bounded model checker.