A cut-off approach for bounded verification of parameterized systems (ICSE 2010) - A Short Review

A cut-off approach for bounded verification of parameterized systems. - Qiusong Yang, Mingshu Li

In this paper a new approach based on forward bounded reachability analysis is proposed for verification of parameterized systems. Experimental results show improvements in verification efficiency as a result of introduction of new cut offs on the maximum length of paths.

For the notations used in the paper, the properties of parameterized systems are expressed in property automata, whose accepting languages (paths leading to trap states) prescribe undesirable behaviour of verified system. The overall approach starts with construction of an extended reachability graph (ERG), which is the synchronous product of the property automaton and the parameterized system. It models the execution of control processes and regulated replications of a parameterized system and their execution’s impact on the property automaton. Instead of using a complete ERG a set of increasingly refined abstractions to it is sequentially generated.  In order to abstract the global state of the parameterized system a notion of configuration is introduced as follows

-          Configuration is a vector of the form c= where ‘s’ is a state vector and ‘a’ is a counter vector.

-          These configuration form the vertices of the ERG while the edges of the graph represent the transitions between these configurations

-          It can  be shown that is possible to calculate the configurations inductively from a finite bounded ERG

The authors state and prove a theorem in the paper which shows that only a finite bounded ERG is needed in order to prove the property.

The given algorithm is implemented in java and compared with other existing algorithms for verification of parameterized systems. The results of such a comparison show that FBRA out performs the known methods in many of the examples. But in a few cases it is indeed slower which the authors attribute to the enumeration of all states in ERGs.  As future work they propose to adopt some of the strategies used to optimize the FBRA algorithm.