LIP6 1997/011

• 学术报告 «"Model Checking" et Systèmes Répartis Paramétrés»
• I. Vernier
• 17 pages - 1997-7-26 - document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.011.ps.gz 344 Ko
• 联系方式 Isabelle.Vernier (at) nulllip6.fr
• Ancien Thème : SRC
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.