LIP6 2005/003

• Rapports de recherche
  Transformation de propriétés CTL lors d'une méthode de conception incrémentale
• C. Braunstein, E. Encrenaz
• 17 pages - 24/05/2005- document en - http://www.lip6.fr/lip6/reports/2005/lip6-2005-003.pdf - 375 Ko
• Contact : cecile.braunstein (at) nulllip6.fr
• Ancien Thème : ASIM
Cet article formalise une méthode de conception incrémentale de traducteurs de protocole VCI en protocole de bus PI (appelés wrappers VCI-PI) et présente leur hiérarchisation du plus simple au plus complexe. A chacun de ces wrappers est associé un ensemble de propriétés CTL représentant une spécification de leur comportement. L'objectif de cet article est d'explorer les relations entre propriétés satisfaites respectivement sur un wrapper simple et un wrapper plus complexe. Nous montrons comment, une propriété vérifiée sur un modèle complexe peut être dérivée d'une propriété vérifiée sur un modèle simple, et réciproquement. Nous proposons des règles de transformation de propriétés qui ont été automatisées et appliquées à des systèmes matériels intégrant ces convertisseurs VCI-PI dans un contexte d'analyse de non-régression.
• Mots clés : Logique CTL, Relation de simulation, Conception et vérification de système
• Directeur de la publication : Francois.Dromard (at) nulllip6.fr