Keywords

1 Introduction

Software, as carrier of information technology, bears the mission of interactions between human and computers. It has been widely used in people’s daily life, as well as in industrial production, aviation, spaceflight and so on. The growing demand for software has led to its greater complexity and larger scale. At the same time, ensuring dependability of software is becoming a strong requirement in many fields. As a result, the software designers face with new challenges at the stages of design, implementation and maintenance of software development these years.

Z [1–5] is a formal specification language used for describing computer programs and computer-based systems in general. Theorem proving [6–8] and animation [9–11] are two main categories of analysis methods for Z notation. The former usually uses predicate logic reasoning to prove the static properties of a Z model. The latter employs a query approach to confirm the expected system behavior by accepting or denying the manually input operations. The decisions are made depending on whether there is any inconsistency between the specification of the operation input and the global constraints of the Z model. These two categories of analysis methods are both unable to automatically verify the temporal properties of a given Z model.

Model checking [12], or property checking, is a technology dealing with the following problem: given a model of a state transition system, exhaustively and automatically check whether this model meets a given formula. Usually, the formula describes temporal properties such as safety and liveness [13]. Because of its conciseness and efficiency, model checking technology has been widely adopted to verify temporal properties of hardware and software systems for over three decades.

Because Z lacks the ability of describing system temporal behavior, building a proper state transition system is the primary step to study the model checking method on Z. A state transition system based on FA (Finite Automata) can describe the run-time behavior of software, but it is insufficient in describing data constraints, comparing with Z’s syntax based on set theory and first-order logic. Some of the current studies on model checking Z are based on transforming Z to a middle language that can be model checked by existing tools [14]. Other related works use new structures such as ZIA [15, 16], which is a combination model of Z notation and interface automata targeted at component based systems. By combining Z and state transition structures, we can establish a more comprehensive system model, and study its model checking method accordingly. However, the existing researches have not implemented automatic model transformation between Z and those hybrid models, which is insufficient for industrial usage.

In this paper, we design and implement a prototype system ZDVS. Firstly, we define a formal model ZA (Z-Automata) combining Z and FA (Finite Automata). The generation algorithm from the basic structures of Z to ZA is studied to enhance the practical usage of our hybrid model. Further on, a model checking algorithm ZAMC is proposed to automatically verify the temporal/data constraints within the structure and behavior specified by ZA. Finally, a case study is used to illustrate the correctness and feasibility of ZDVS.

2 ZA Model

To verify dynamic temporal behavior of a system, we take the advantages of the predicate logic description ability of Z notation and the temporal description ability of FA. In this section, we give the formal definition of ZA model and design a generation algorithm to transform Z static model to ZA.

2.1 Formal Definition of ZA

In order to facilitate the study of model checking Z, and to establish a formal relationship between Z specification and ZA model, we present a formal definition of ZA. First of all, we define some useful notations in Definition 1, to help the definition of ZA. Secondly, we define a simplified structure of Z models as ZA static in Definition 2, to delineate the element set we need to map to FA.

Definition 1.

Assume that a Z schema declaresas \( x_{1}, \ldots, x_{n} \) its variables, the invariants in the schema can be seen as an n-ary predicate. We use the form \( S_{{p_{n} }} \) to state the n-ary prediction. In particular, we denote the pre-conditions of an operation schema Op as \( pre_{Op} \), and the post-conditions as \( post_{Op} \).

Definition 2.

A ZA Static Model

$$ ZAstatic = (State, Operation) $$
(1)

consists of the following elements:

  • State is a finite set of state spaces. Its elements correspond to the state schemas in a Z specification.

  • Operation is a finite set of operations. Its elements correspond to the operation schemas in a Z specification.

We has designed and implemented a Z notation parser as a crucial component of ZDVS, to analyze an input Z model and transform it to a ZA static model written by C++.

The formal definition of ZA is given as follows.

Definition 3.

A ZA Model

$$ {\text{ZA}} = (S,S_{0} ,\Sigma ,\delta ,F,\text{M}) $$
(2)

consists of the following elements:

  • S is a finite set of states.

  • \( S_{0} \subseteq S \) is a finite set of initial states.

  • \( \Sigma \) is a finite set of operations.

  • \( \updelta \subseteq (S \times \varSigma \times S) \) is a finite set of state transitions. A state transition \( (s,a,s^{{\prime }} ) \in\updelta \) represents that system transits from state s to \( s^{{\prime }} \).

  • F is a finite set of end states.

  • M denotes a binary relationship between S, \( \varSigma \) and the elements in ZA static , such that \( {\text{M}} = (F_{s} ,F_{\Sigma } ) \). The definitions of its tuples are as follows:

    F s is a mapping from S to State, i.e.,

    $$ F_{s} \left( s \right) = state,\;{\text{where}}\,s \in S,\,state \in State $$
    (3)

\( F_{\varSigma } \) is a mapping from \( \varSigma \) to Operation, i.e.,

$$ F_{\varSigma } \left( a \right) = op,\,{\text{where}}\,a \in\Sigma, \,op \in Operation $$
(4)

According to Definition 3, the prerequisite of a state transition \( (s,a,s^{{\prime }} ) \in\updelta \) is that state s meets the pre-conditions, and \( s^{{\prime }} \) meets the post-conditions of operation a, that is, \( s| = pre_{{F_{\Sigma } (a)}} \) and \( s^{{\prime }} | = post_{{F_{\Sigma } (a)}} \) hold.

2.2 The Generation of ZA Model

After the formal definition of ZA model, we propose a generation algorithm which builds a ZA model from the ZA static model. The input of the algorithm is ZA static  = (State, Operation), and the output is a ZA model.

The procedure of the generation is described as follows:

  • Step 1. Initialization phase. Initialize s 0 and a stack St;

  • Step 2. Add s 0 to S 0 and S. Build the one-to-one relationship between Operation and \( \Sigma \), and the relationship between State and S.;

  • Step 3. Push s 0 onto St;

  • Step 4. Get the top element s of St, while St is not empty;

  • Step 5. For each operation a i in \( \Sigma \), if \( s\left| { = pre_{{F_{\Sigma } (a_{i} )}} } \right. \) is true, perform a i on s and get a new state \( s^{{\prime }} \);

  • Step 6. If \( s^{{\prime }} | = post_{{F_{\Sigma } (a)}} \) is true and it meets the global constrains, add \( (s,a_{i} ,s^{{\prime }} ) \) to \( \updelta \);

  • Step 7. If \( s^{{\prime }} \) doesn’t exist, add \( s^{{\prime }} \) to S and push it onto St. If it’s an end state, add it to F;

  • Step 8. Go to step 5, until all operations in \( \Sigma \) are considered;

  • Step 9. Go to step 4, until St is empty;

  • Step 10. Output the ZA model.

Figure 1 gives the pseudo code of ZA model generation algorithm according to the above procedure.

Fig. 1.
figure 1

The pseudo code of ZA model generation algorithm

Full size image

3 Model Checking ZA

In this section, we define a set of temporal logic formulas called ZATL (Z-Automata Temporal Logic) to describe the expected temporal properties of the system. Further on, a model checking algorithm called ZAMC (Z-Automata Model Checking) is proposed to perform the verification towards such properties.

3.1 Temporal Logic Formula Towards ZA

First of all, we define some useful notations in Definition 4, to help the definition of ZATL.

Definition 4.

A finite state sequence \( \pi = (s_{0} ,s_{1} , \ldots ,s_{n} ) \) is used to describe a state transition path in a ZA model, where \( s_{i} \in S \) and \( \left( {s_{i} ,a,s_{i + 1} } \right) \in\updelta (i \in N \), \( i < n \)). We define that \( \pi \) and each state \( s_{i} \) in \( \pi \) satisfy the relation \( \pi \left[ i \right] = s_{i} \). We denote \( \varPi (s) \) as a set of paths starting from \( s \), that is, \( \mathop \prod \nolimits \left( s \right) = \left\{ {\pi |\pi \left[ 0 \right] = s} \right\} \). By \( [[\varphi ]]_{s} \) we denote a set of states where formula \( \varphi \) holds. By \( [[\varphi ]]_{\pi } \) we denote a set of paths in which all states satisfy \( \varphi \).

ZATL compliances with the following elements:

  • ⃞ is the always operator. ⃞φ means that φ is always true.

  • \( \diamond \) is the sometimes operator. \( \diamond\varphi \) means that φ is sometimes true.

  • A is the all quantifier.

  • E is the exist quantifier.

Definition 5.

The syntax of ZATL is defined as follows:

  • The atomic proposition \( \varphi_{{p_{n} }} \) is a ZATL formula.

  • If \( \varphi \) and \( \psi \) are ZATL formulas, so are \( \neg \varphi \), \( \varphi \wedge \psi \), \( \varphi \vee \psi \).

  • If \( \varphi \) is a ZATL formula, so are \( {\text{A}} \square \varphi \), \( {\mathbf{E}} \square \varphi \), \( {\mathbf{A}} \diamond \varphi \), \( {\mathbf{E}} \diamond \varphi \).

  • If and only if the above rules are used for limited times, we get a ZATL formula.

Definition 6.

The semantics of ZATL is defined as follows:

  • \( [[\varphi_{{p_{n} }} ]]_{s} = \left\{ {s\left| \varphi \right| = F_{S} (s)_{{q_{m} }} } \right\} \), where p and q are predicates, \( n,m \in N \);

  • \( [[\neg \varphi ]]_{s} = S - [[\varphi ]]_{s} \);

  • \( [[\varphi_{1} \wedge \varphi_{2} ]]_{s} = [[\varphi_{1} ]]_{s} \cap [[\varphi_{2} ]]_{s} \);

  • \( [[\varphi_{1} \vee \varphi_{2} ]]_{s} = [[\varphi_{1} ]]_{s} \cup [[\varphi_{2} ]]_{s} \);

  • \( \left[ {\left[ {{\mathbf{A}} \square \varphi } \right]} \right]_{\pi } = \left\{ {\pi |\forall \pi \in \prod \left( {s_{0} } \right) \cdot (\forall s \in \pi \cdot (s_{{p_{n} }} | = \varphi ))} \right\} \)

  • \( [[{\mathbf{A}} \diamond \varphi ]]_{\pi } = \left\{ {\pi |\forall \pi \in \mathop \prod \nolimits \left( {s_{0} } \right) \cdot (\exists s \in \pi \cdot (s_{{p_{n} }} | = \varphi ))} \right\} \);

  • \( [[{\mathbf{E}} \square \varphi ]]_{\pi } = \left\{ {\pi |\exists \pi \in \mathop \prod \nolimits \left( {s_{0} } \right) \cdot (\forall s \in \pi \cdot (s_{{p_{n}}} | = \varphi))} \right\} \)

  • \( [[{\mathbf{E}} \diamond \varphi ]]_{\pi } = \left\{ {\pi |\exists \pi \in \mathop \prod \nolimits \left( {s_{0} } \right) \cdot (\exists s \in \pi \cdot (s_{{p_{n}}} | = \varphi))} \right\} \).

The first four formulas represent the composition mode of \( {\varphi } \). The last four formulas are temporal logic formulas used to describe properties of system.

\( \mathbf{A} \square \phi \) denotes that all the states in the system satisfy \( \varphi \). \( \mathbf{A} \diamond \varphi \) denotes that there is at least one state satisfying \( \varphi \) in every path of the system. \( \mathbf{E} \square \varphi \) denotes that there is at least one path in which all the states satisfy \( \varphi \). And \( \mathbf{E} \diamond \varphi \) denotes that there is at least one state in the system satisfying \( \varphi \). These formulas can be used to describe the dependability properties of system such as liveness and safety.

3.2 ZAMC Algorithm

In order to verify whether the given system satisfies the property described by a ZATL formula, we propose a model checking algorithm based on counterexample searching strategy. For each formula we design different searching strategies depending on its semantics.

  1. (1)

    Input formula 1: \( {\varphi }^{{\prime }} = {\mathbf{A}} \square {\varphi }. \)

Formula 1 denotes that formula \( \varphi \) holds for all the states in the system. If the given ZA model meets this condition, the system satisfies formula \( \varphi^{\prime } \). Otherwise, the system doesn’t satisfy \( \varphi^{\prime } \). The counterexample of formula 1 is a state on which formula \( \varphi \) doesn’t hold. The verification procedure of formula 1 is as follows.

  • Step 1.1. Get an unprocessed element s in set S;

  • Step 1.2. If s doesn’t satisfy \( \varphi \), the system doesn’t satisfy \( \varphi^{\prime } \). Output current state s as a counterexample, and the verification ends up with false;

  • Step 1.3. If s satisfies \( \varphi \), go to Step 1.1;

  • Step 1.4. Output true of this verification.

  1. (2)

    Input formula 2: \( \varphi^{\prime} = {\mathbf{A}} \diamond \varphi \).

Formula 2 denotes that there is at least one state satisfying \( \varphi \) in every path of the system. If the given ZA model meets this condition, the system satisfies formula φ’. Otherwise, the system doesn’t satisfy φ’. The counterexample of formula 2 is a path in which none of the states satisfies \( \varphi \). The verification procedure of formula 2 is as follows.

  • Step 2.1. If initial state \( s_{0} \) satisfies \( \varphi \), the system satisfies formula φ’. Verification process ends, and output true;

  • Step 2.2. Otherwise, put s 0 into queue Q;

  • Step 2.3. While Q is not empty, get state s from Q;

  • Step 2.4. If s doesn’t satisfy \( \varphi \), update current searching path. If \( s \in F \), we find a counterexample. So the verification ends up with false;

  • Step 2.5. If s satisfies \( \varphi \), put all unprocessed successor states of s into Q;

  • Step 2.6. Go to Step 2.3, until Q is empty;

  • Step 2.7. If we find a counterexample, output the counterexample according to searching path. Otherwise, output true.

  1. (3)

    Input formula 3: \( {\varphi }^{{\prime }} = {\mathbf{E}} \square {\varphi }. \)

Formula 3 denotes that there is at least one path in which all the states satisfy \( \varphi \). If the given ZA model meets this condition, the system satisfies formula φ’. Otherwise, the system doesn’t satisfy φ′, that is, in every path of the system there is at least one state that doesn’t satisfy \( \varphi \). As a result, we can formalize it as \( {\mathbf{A}} \diamond \neg \varphi \), thus the verification of formula 3 can use the verification procedure of formula 2. Firstly, we verify whether the system satisfy formula \( {\mathbf{A}} \diamond \neg \varphi \). Then, invert the result as output.

  1. (4)

    Input formula 4: \( \varphi^{\prime} = {\mathbf{E}} \diamond \varphi \).

Formula 4 denotes that there is at least one state in the system satisfying \( \varphi \). If the given ZA model meets this condition, the system satisfies formula \( \varphi^{{\prime }} \). Otherwise, the system doesn’t satisfy \( \varphi^{{\prime }} \), that is, none of the states satisfies \( \varphi \). The verification procedure of formula 4 is as follows.

  • Step 4.1. Get an unprocessed element s in set S;

  • Step 4.2. If s satisfies \( \varphi \), the system satisfy \( \varphi^{{\prime }} \). And the verification ends up with true;

  • Step 4.3. If s doesn’t satisfy \( \varphi \), go to Step 4.1;

  • Step 4.4. Output false of this verification. Any state can be used as a counterexample.

Figure 2 gives the procedure of ZAMC.

Fig. 2.
figure 2

The procedure of ZAMC

Full size image

4 Design and Application of ZDVS

Based on the ZA model and the ZAMC algorithm, we realize a prototype system called ZDVS (Z Dynamic Verification System). In this section, we present its framework and procedure. A case study is used to illustrate the correctness and effectiveness of our method.

4.1 Framework of ZDVS

ZDVS has three main modules, including the modeling module, the verification module and the user interface module. Figure 3 gives the flow diagram of ZDVS.

Fig. 3.
figure 3

The flow diagram of ZDVS

Full size image

Firstly, we transform Z specification to ZA static model by implementing a parser in the modeling module, to analyze Z notation and transform it to ZA static model written by C++. Then, we implement the ZA model generation algorithm in the modeling module to build the corresponding ZA model.

In the verification module, we design a command parser to obtain the input ZATL formulas (through the user interface module), and implement the ZAMC algorithm to verify the ZA model.

The user interface module provides the necessary interaction between user and system, such as the input of ZATL formulas, and the display of the counterexamples if the verification ends up with false.

4.2 A Case Study

In this section, we describe the modeling and analysis procedure of a case study to illustrate the correctness and effectiveness of ZDVS. The inputs of ZDVS are Z specification represented by LaTeX and ZATL formula \( \varphi \), while the output is the result of model checking. If the result is false, it also gives a counterexample.

The case study contains 4 schemas as shown in Fig. 4, including a state schema and 3 operation schemas. The corresponding ZA model generated by ZDVS contains 30 states and 3 actions.

Fig. 4.
figure 4

Z specification of the instance

Full size image

We use 4 temporal logic formulas as inputs of the model checking process, which are listed as follows.

  • \( {\mathbf{A}} \square \text{var}1\le3 \), denotes that var1 in all the states of the system is equal or greater than 3.

  • \( {\mathbf{A}} \diamond \text{var}1>4 \), denotes that for every path of the system there is at least one state in which var1 is greater than 4.

  • \( {\mathbf{E}} \square {\text{var1}} \ge {\text{var2}} \), denotes that there is at least one path in which all the states satisfy var1 ≥ var2.

  • \( {\mathbf{A}} \diamond \) var1 ≥ var2 && var2 > 2, denotes that there is at least one state in the system satisfying var1 ≥ var2 && var2 > 2.

Figure 5 shows the verification result of formula \( {\mathbf{A}} \diamond \) var1 > 4. Since the result is false, the system outputs a counterexample.

Fig. 5.
figure 5

Verification result

Full size image

Illustration on the case study shows that the proposed ZA model can enhance the descriptive power by combining Z notation and FA. The prototype system ZDVS is able to correctly parse the input Z specification and generate the corresponding ZA model, accept and analyze the input ZATL formulas, and verify the system temporal properties automatically and effectively.

5 Discussion and Conclusion

In order to verify the temporal properties of Z model, this paper designs and implements a prototype system ZDVS to perform the model transformation and model checking on a proposed hybrid software model ZA. Our main contributions are as follows:

  1. 1.

    A formal software model called ZA is defined by combining Z notation and FA. The proposed ZA model can specify not only static structure and operation specifications, but also temporal constraints of the targeted system. A generation algorithm is designed to build ZA model from ZA static , a simplified structure of Z specification.

  2. 2.

    A model checking algorithm towards the ZA model is proposed. Firstly, a temporal logic called ZATL is defined to describe the temporal properties of the ZA model. Then, we propose a model checking algorithm called ZAMC to verify the ZATL formulas.

  3. 3.

    A prototype system called ZDVS is realized to perform our proposed methods. A case study is used to illustrate the correctness and effectiveness of ZDVS.

Future work of this paper includes further study on hybrid software models and their temporal logic, and the performance enhancement of their model checking algorithms.