![[Maison.png]](../../images/Maison.png)
Back to Home| Abstract The use of formal verification methods has been studied for several decades now as a promising mean to improve software quality, particularly in the context of concurrent systems. Among them, approaches based on finite state-machine representations certainly belong to the most popular. Unfortunately, the state machine representation of a concurrent system grows exponentially in size with the number of its concurrent components. In this technical report we give an overview of two of the most important techniques proposed to fight against this combinatorial state proliferation, commonly known as the state space explosion. The first one, based on Binary Decision Diagrams [BCM90], is a representative of symbolic approaches. These techniques use compact representations of state regions and transition relationships to reduce the memory requirement of verification algorithms. We first introduce general BDDs in an informal way using a small example. Then we show how those BDDs can be used to code a small state transition system. The second state reduction technique we present is based on partial unfolding of Petri Nets [McMill95]. It belongs to the partial order reduction methods. Such approaches are based on the idea that in most cases the total interleaving of concurrent actions is not needed to check a given property on a system. In such cases, a total interleaving distinguishes between action sequences and their intermediary state counterparts that are equivalent from the point of view of the checked property. In this report we use a small concurrent system expressed with two state machines to show how the partial unfolding technique can be applied to it. We also introduce the informal concept of 'unambiguous past / divergent future' to sum up the 'self conflict freedom' and 'forward conflict freedom' rules introduced in [McMill95]. |
Back to Home