Formalisation d’une Approche Compositionnelle de Patrons de Propriétés - ENSTA Bretagne - École nationale supérieure de techniques avancées Bretagne Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

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

Résumé

Pour faciliter et encadrer l’expression des propriétés formelles, des alternatives aux logiques temporelles, telles que LTL ou CTL, ont été proposés, au prix de la réduction de l’expressivité. Celles-ci proposent des langages d’expression de propriétés basés sur des patrons de définition. Dans le but d’étendre l’expressivité des patrons proposés, nous avons conçu un langage de type DSL (Domain Specific Language) nommé CDL (Context Description Language). Ce langage permet une expression de propriétés de sûreté basée sur une extension des patrons proposés par Dwyer et al. Les propriétés sont traduites en automates observateurs et exploités par l’explorateur de modèles OBP (Observer-Based Prover). Pour pouvoir valider formellement la transformation des propriétés, nous avons formalisé, avec l’outil COQ, la sémantique des patrons dans une approche compositionnelle.
Fichier non déposé

Dates et versions

hal-01326333 , version 1 (03-06-2016)

Identifiants

  • HAL Id : hal-01326333 , version 1

Citer

Djamila Baroudi, Philippe Dhaussy, Nait Bahloul Safia. Formalisation d’une Approche Compositionnelle de Patrons de Propriétés. AFADL 2016, i, Jun 2016, Besançon, France. ⟨hal-01326333⟩
361 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More