Formalisation d’une Approche Compositionnelle de Patrons de Propriétés
2016
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
5
References
0
Citations
NaN
KQI