Computer Aided Verification of Automata (CAVA)
The CAVA project aims at formalising and verifying important algorithmic parts of automata theory as well as its applications in model checking. These formalisations are done in higher order logic using the interactive theorem prover Isabelle. The algorithms are formalised on an mathematical, abstract level, using mainly sets and relations. At the same time these formalisations are intended to be executable. This means, that Isabelle is able to automatically generate programs in Haskell, OCaml or SML from these formalisations.
The generated programs are intended to be reference implementations that can be used to test the correctness of other implementations. Therefore, all algorithms that are needed for model checking have to be verified. Otherwise a mixture of verified and unverified components would undermine the trust in the reference implementation.
It is planed to formalise key algorithms of the following fields of automata theory and model checking:
1) Finite Automata and Regular Expressions
The formalisation of finite automata is intended to provide key datastructures and algorithms that are used by different model checking algorithms. The algorithms on finite automata we intend to formalise include operations like Boolean combinations, minimisation, translation of regular expressions into finite automata, ... . Moreover, it is planed to implement an automata based decision procedure for equations of regular expressions.
2) Büchi-automata and other ω-automata
ω-automata (finite automata over infinite words) and in particular Büchi-automata are the basis of automata based model checking algorithms for linear temporal logics like LTL. This project will provide verified implementations of Boolean combinations of ω-automata. The biggest challenge is verifying a negation algorithm for Büchi-automata. Other types of ω-automata (like generalised Büchi-, Muller-, Rabin- or Streett-automata) will be formalised as far as needed. The CAVA project aims also at verifying translation algorithms between these types of ω-automata.
In contrast to finite automata on finite words, efficient decision procedures for the emptiness of ω-automata are non-trivial. Because such emptiness checks play a vital role for model-checking, they are considered separately as goal 4.
3) Translation of Logic into Automata
The translation of LTL in Büchi-automata or alternating ω-automata is a first important step for automata based model checking. As part of this project efficient translations will be formalised. Similarly, we plan to translate linear arithmetic into finite automata. This translation forms the basis of infinite state model checking algorithms.
4) Finite State Model Checking
The translation of LTL into Büchi-automata (see Goal 3) reduces the model checking problem of finite state systems to the emptiness check of Büchi-automata (see Goal 2). However, the resulting automata are very large and memory-efficient algorithms very sophisticated. Therefore, the combination of Goals 2 and 3 as well as the implementation of efficient algorithms are a goal in its own right.
5) Model Checking Procedural and Concurrent Systems
The approach of Bouajjani et al. [1] for model checking Büchi-pushdown automata will be formalised as part of the CAVA project. This approach uses finite automata on finite words for encoding and manipulating sets of configurations. Therefore, the library developed as Goal 1 is needed here. For software model checking abstraction is of essence. Weighted automata [2, 3] have been used very successfully to implement abstraction methods. We plan to provide verified implementations of these methods.
The reference implementations developed as part of the CAVA project have to be sufficiently efficient to run non-trivial test cases. In order to be reusable for other researchers and different projects, the formalisation of automata theory should be as abstract as possible. All algorithms and proofs will be publicly available in the Archive of Formal Proofs.
Bibliography
[1] | A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In A. W. Mazurkiewicz and J. Winkowski, editors, CONCUR, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997. |
[2] | T. W. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program., 58(1-2):206-263, 2005. |
[3] | S. Jha, S. Schwoon, H. Wang, and T. W. Reps. Weighted pushdown systems and trust-management systems. In H. Hermanns and J. Palsberg, editors, TACAS, volume 3920 of Lecture Notes in Computer Science, pages 1-26. Springer, 2006. |
Verified Model Checkers
The first goal consists of developing an efficient (competitive) verified model checker for LTL. This is the continuation of the CAVA project with more ambitious goals: We want to improve our reference implementation which is 1-2 orders of magnitude slower than SPIN to be as efficient as SPIN while still being fully verified.
The second goal is to develop a verified probabilistic model checker for PLTL (probabilistic LTL), PCTL, and PCTL* which can be used as reference implementations. We want to model our implementation after the popular (unverified) probabilistic model checkers PRISM and MRMC. This is the merger of the CAVA and the PM (probabilistic model checking) project. The focus lies on transforming the mathematical foundation from the PM project into executable algorithms, although these may to yet be competitive with PRISM.