Techniques avancées pour la vérification de systémes a nombre d'états infini
Project Period: 20. 2. 2008 - 31. 12. 2009
Project Type: grant
Code: MEB 020840
Agency: Barrande - Czech-French programme of integrated actions
formal verification, infinite-state systems, model checking
One of the currently most studied approaches to formal verification is model checking, which is attractive by its high degree of automation and at the same time a high degree of precision. Most of the research on model checking has so-far concentrated on systems with possibly large, but finite state spaces. However, many systems that one encounters in practice are infinite-state. Infinity can arise due to dealing with various kinds of unbounded data structures such as push-down stacks needed for dealing with recursive procedures, FIFO (and other kinds) of communication channels or waiting queues, unrestricted counters (or integer variables), dynamic linked data structures (such as lists or trees). Yet another source of infinity is then dealing with various kinds of parameters (such as the maximum value of some variable, the maximum length of a queue, or the number of processes in a system). Consequently, techniques applying model checking in the area of infinite-state systems have begun to appear as well.
Among the most successful approaches to infinite-state model checking that have been proposed so-far, an important role is played by symbolic methods based on using various formalisms (such as logics, automata, grammars, etc.) for a finite representation of infinite sets of reachable states. Members of the project team have significantly contributed to the research in this area by several internationally recognised and cited results including original methods of symbolic, automata-based model checking combined with automated abstraction (the so-called abstract regular model checking---ARMC, methods based on automatic inference (learning) of regular languages representing sets of reachable states from their samples, and a series of methods for verifying programs manipulating dynamic linked data structures (using ARMC, automated detection of repeated memory patterns, or different types of extended automata with constraints).
The efficiency of the current methods of model checking of infinite-state systems is, however, still far from a broad practical applicability, and the classes of systems and their properties of interest on which these methods are applicable are also restricted. Therefore, the goal of the project is to contribute to the research on methods of model checking of infinite-state systems in order to significantly lift their current restrictions both in terms of efficiency as well as generality.
In particular, in order to contribute to an increased efficiency of the existing symbolic model checking approaches for infinite-state systems, the project will, e.g., consider development of symbolic model checking approaches based on non-deterministic automata (avoiding the determinisation step that turns out to be one of the most expensive steps in the current approaches). This implies a need of development of all the needed automata operations (such as emptiness checking, inclusion checking, minimisation, abstraction) for different kinds non-deterministic automata (word automata, tree automata, etc.). In the area of increasing the generality of the existing approaches, the project will consider both dealing with more general systems (e.g., programs with unrestricted dynamic linked data structures and integer variables) as well as dealing with more complex properties to be checked (such as termination or liveness properties). In order to do so, the project will examine various extensions of the current automata and logics (e.g., combining various classes of automata and logics describing in a qualitative way the structure of system configurations with various numerical constraints) and also of the procedures of dealing with them (including advanced decision procedures over logics, new abstraction and inference methods over automata, etc.).
Habermehl Peter (UPAR7) , team leader
Bouajjani Ahmed (UPAR7)
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Touili Tayssir (LIAFA UP7/CNRS)