LIP6 2005/008

• Reports
  Diagrammes de Décision de Données pour l'analyse de systèmes ProMeLa
• V. Beaudenon, E. Encrenaz, S. Taktak
• 13 pages - 06/28/2005- document en - http://www.lip6.fr/lip6/reports/2005/lip6-2005-008.pdf - 355 Ko
• Contact : Vincent.Beaudenon (at) nulllip6.fr
• Ancien Thème : ASIM
In this paper, we show how to verify CTL properties, using symbolic methods, on systems written inProMeLa. Symbolic representation is based on Data Decision Diagrams (DDDs) which are n-valued DAGs designed to represent dynamic systems with integer domain variables. We describe principal components used for the verification of ProMeLa systems (DDD, representation of ProMeLa programs with DDD, the transposition of the execution of ProMeLa instructions into DDD). Then we compare and contrast our method with the model checker SPIN or classical BDD techniques, to highlight what system classes whether SPIN or our tool is more relevant for.
• Keywords : SPIN, CTL, Symbolic Verification Methods, BDDs, DDDs
• Publisher : Francois.Dromard (at) nulllip6.fr