Séminaires
Séminaire du 19 Janvier 2007
Lieu
LIP6: comment y aller
Programme
14h00-15h00: Kurt Jensen (Univ. Aarhus, Denmark):
« Introduction to two "smart" state space techniques »
Abstract: model checking based on state space construction is one of the most promising methods for verification of formal models. The basic idea is to construct a directed graph that contains a node for each reachable state and an arc for each possible transition from one state to another. The construction and analysis of state spaces can be fully automated and this means that the user does not need to know the often complex and non-trivial mathematics behind the different construction and analysis techniques. This makes the method well-suited for industrial use. The main drawback of state spaces is the fact that they often become unmanageable large -- in particular when system parameters such as the number of modelled processes are increased. To cope with this problem a number of different techniques have been developed -- making it possible to substitute brute-force construction with different kinds of "smartness". The talk will give an introduction to two such techniques. The first technique builds on the observation that the modelled system often contains some kind of symmetry or other regularity. This implies that some states are similar enough to be considered equivalent. Then it is sufficient to have a node in the state space for each equivalence class of states -- instead of having a node for each individual state. The consequence is an often dramatic decrease in the use of both time and memory. We can investigate the same behavioural questions as for full state spaces, but only up to equivalence. As an example, we cannot ask whether it is possible to reach a given state -- only whether it is possible to reach a state that is equivalent to it. The second technique uses a progress measure to allow removal of constructed states that cannot be reached again. In this way there will be room for new states and it is possible to sweep through a larger state space without running into memory problems. It is interesting that the use of this technique not only reduces the memory consumption but also time. The reason is that there are fewer states to consider when we have to determine, whether a newly constructed state is identical/similar to one of those which we already have seen.
15h00-15h30 : Alexandre Hamez (LIP6) : « Distributed model checking with libDMC »
Abstract: model checking offers a way to automatically prove that a modeled system behavior is correct by verifying properties. However, it suffers of the so-called state space explosion problem, caused by a intensive use of memory. Many solutions have been proposed to overcome this problem like symbolic representations with decisions diagrams. But these methods can rapidly lead to a unacceptable time consumption. Distributed model checking is a way to overcome both memory and time consumptions by using aggregated ressources of a dedicated cluster. However, re-writing an entire model checker is a difficult. So, there is a need to identify what are the most common need of existing model checkers to ease their distribution. In this perspective, we introduce libDMC, a library dedicated to distributed model checking. We present its generic design and its first results.