LIP6 2005/003

• Reports «Transformation de propriétés CTL lors d'une méthode de conception incrémentale»
• C. Braunstein, E. Encrenaz
• 17 pages - 05/24/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
This paper formalizes an incremental approach to design VCI to PI protocol converters (VCI-PI wrappers) and presents a hierarchy of wrappers ranking from the simplest one up to the most complex one. In order to formally verify the correctness of a wrapper, a set of CTL properties is assigned to it. The purpose of the paper is to explore how, given a property that is true in a simple model, a new property, satisfied in a more complex model, can be derived from the first one, and reciprocaly. We propose some transformation rules to build new properties satisfied on more complex models. The properties transformation have been automated and applied in the context of non-regression analysis of VCI-PI wrappers.