Formalisation d’une Approche Compositionnelle de Patrons de Propriétés

Pour faciliter et encadrer l’expression des proprietes formelles, des alternatives aux logiques temporelles, telles que LTL ou CTL, ont ete proposes, au prix de la reduction de l’expressivite. Celles-ci proposent des langages d’expression de proprietes bases sur des patrons de definition. Dans le but d’etendre l’expressivite des patrons proposes, nous avons concu un langage de type DSL (Domain Specific Language) nomme CDL (Context Description Language). Ce langage permet une expression de proprietes de surete basee sur une extension des patrons proposes par Dwyer et al. Les proprietes sont traduites en automates observateurs et exploites par l’explorateur de modeles OBP (Observer-Based Prover). Pour pouvoir valider formellement la transformation des proprietes, nous avons formalise, avec l’outil COQ, la semantique des patrons dans une approche compositionnelle.