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

Autor: Baroudi, Djamila, Dhaussy, Philippe, Safia, Nait Bahloul
Přispěvatelé: Billon-Coat, Annick, Université de Mostaganem, Lab-STICC_ENSTAB_CACS_MOCS, IDM, Pôle STIC [Brest] (STIC), École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Université européenne de Bretagne - European University of Brittany (UEB)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Université européenne de Bretagne - European University of Brittany (UEB)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) (Lab-STICC), Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Télécom Bretagne-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université européenne de Bretagne - European University of Brittany (UEB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-Télécom Bretagne-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2016
Předmět:
Zdroj: AFADL 2016
AFADL 2016, i, Jun 2016, Besançon, France
Popis: International audience; Pour faciliter et encadrer l’expression des propriétés formelles, des alternatives auxlogiques temporelles, telles que LTL ou CTL, ont été proposés, au prix de la réductionde l’expressivité. Celles-ci proposent des langages d’expression de propriétés basés surdes patrons de définition. Dans le but d’étendre l’expressivité des patrons proposés, nousavons conçu un langage de type DSL (Domain Specific Language) nommé CDL (ContextDescription Language). Ce langage permet une expression de propriétés de sûreté baséesur une extension des patrons proposés par Dwyer et al. Les propriétés sont traduites enautomates observateurs et exploités par l’explorateur de modèles OBP (Observer-BasedProver). Pour pouvoir valider formellement la transformation des propriétés, nous avonsformalisé, avec l’outil COQ, la sémantique des patrons dans une approche compositionnelle.
Databáze: OpenAIRE
Externí odkaz: