LIP6 1997/011
- Reports
"Model Checking" et Systèmes Répartis Paramétrés - I. Vernier
- 17 pages - 07/26/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.011.ps.gz - 344 Ko
- Contact : Isabelle.Vernier (at) nulllip6.fr
- Ancien Thème : SRC
- Keywords : Verification, validation, temporal logic, parameterized systems, Petri nets
- Publisher : Denis.Poitrenaud (at) nulllip6.fr
We propose a solution to solve part of the verification problem for a set of parallel programs that are the instantiations of a same algorithm. The instantiated parameter is the number of processes. All the possible programs are supposed to satisfy the same properties. Petri nets with guarded transitions model the programs. The originality of our method is to build a symbolic graph that allows us to verify temporal properties that concern the behavior of the whole program as well as properties that concern the behavior of a single process. The nodes of the symbolic graph are predicates that represent sets of states.