Research On Automata-based Efficient Model Checking Algorithms

Model Checking is a successful and important technology for system verification automati-cally. The main idea of Model Checking is to search for all the states that a system model can reach, and exhaustively check whether this model meets a given specification. If not, the model checker will supply a counterexample. This thesis focuses on the automata-based (explicit-state) model checking, which is applicable for software systems. Given a system model, according to the various properties to be verified, different kinds of model checking algorithms are required, in-cluding reachability algorithm, refinement checking algorithm and emptiness checking algorithm for model checking based on temporal logic。 Among them, refinement checking and emptiness checking algorithms still suffer from the following problems:(1) Refinement checking algorithm is based on subset construction, which is often hampered by the state explosion problem; (2) Current-ly the refinement checking is aimed at the verification of concurrent systems. However, for some more complex systems, like real-time systems with timed constraints (often modeled with timed automata), there is no efficient and complete algorithm to support the refinement checking; (3) The emptiness checking for finite automata has been well studied, however, the emptiness check-ing of timed automata still has some problems to be solved:the non-Zenoness problem (infinite events should not happen in finite time) should be considered in the emptiness checking of timed automata, but there is no efficient algorithm to support it.To address the above problems, this thesis proposes anti-chain based refinement checking algorithms, refinement checking algorithm for timed automata, and a new emptiness checking algorithm for timed automata with the assumption of non-Zenoness, which are shown as follows.1. Refinement checking often relies on the classic subset construction approach, and easily suffers from state space explosion. In this thesis, we study the problem of adopting anti-chain for three kinds of refinement checking, including trace refinement checking, stable failures refinement checking and failures-divergence refinement checking. We show how to reduce the state space using anti-chain, and also prove the correctness of all the algorithms. The experimental results show that the anti-chain based algorithms outperform the algorithms without anti-chain significantly.2. The refinement checking algorithm for timed automata is first proposed in this thesis, which is to decide whether the language of a timed automaton is a subset of that of another timed automaton. The algorithm uses zone abstraction which can efficiently generate a finite state space, which makes the algorithm practical. Though the algorithm is not guaranteed to ter-minate since the determinization of timed automata is undecidable, we show that it does in many cases through both theoretical and empirical analysis. The algorithm also implements simulation reduction based on Anti-Chain and LU-simulation to further improve the perfor-mance. The algorithm has been incorporated into the PAT model checker, and applied to multiple systems to show its usefulness and scalability.3. This thesis proposes a new emptiness checking algorithm for timed automata with the as-sumption of non-Zenoness. Existing approaches on non-Zenoness checking include either introducing an additional clock in the timed automata or additional states, which cause state space explosion. We define a subclass of timed automata, called CUB-TA, and develop an efficient non-Zenoness based emptiness checking algorithm, which does not introduce extra clocks or states. Based on this, it is proved that any timed automaton can be transformed into CUB-TA, and a fast transformation algorithm is proposed. The experiments show that most of the systems in reality are CUB-TA, or can be transformed into CUB-TA with a little cost, therefore the newly proposed algorithm is practical. The experimental results also show the effectiveness of the algorithm.4. A reason of the success of model checking is the support of various model checkers. We have integrated all the above mentioned algorithms into the PAT model checker. With the formal modeling languages and parsing technology realized in PAT, the users can model systems and properties conveniently, and verify the properties efficiently.