Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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

Djamila Baroudi 1, 2 Philippe Dhaussy 3 Nait Bahloul Safia
2 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
3 Lab-STICC_ENSTAB_CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192)
Abstract : 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.
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01326333
Contributeur : Annick Billon-Coat <>
Soumis le : vendredi 3 juin 2016 - 14:35:53
Dernière modification le : mercredi 24 juin 2020 - 16:19:30

Identifiants

  • HAL Id : hal-01326333, version 1

Citation

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⟩

Partager

Métriques

Consultations de la notice

573