OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Assistance à la validation et vérification de systèmes critiques : ontologies et intégration de composants

Kezadri, Mounira. Assistance à la validation et vérification de systèmes critiques : ontologies et intégration de composants. PhD, Institut National Polytechnique de Toulouse, 2013

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
2MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00002354/

Abstract

Les activités de validation et vérification de modèles sont devenues essentielles dans le développement de systèmes complexes. Les efforts de formalisation de ces activités se sont multipliés récemment étant donné leur importance pour les systèmes embarqués critiques. Notre travail s’inscrit principalement dans cette voie. Nous abordons deux visions complémentaires pour traiter cette problématique. La première est une description syntaxique implicite macroscopique basée sur une ontologie pour aider les concepteurs dans le choix des outils selon leurs exigences. La seconde est une description sémantique explicite microscopique pour faciliter la construction de techniques de vérification compositionnelles. Nous proposons dans la première partie de cette thèse une ontologie pour expliquer et expliciter les éléments fondateurs du domaine que nous appelons VVO. Cette ontologie pourra avoir plusieurs autres utilisations : une base de connaissance, un outil de formation ou aussi un support pour le choix de la méthode à appliquer et l’inférence de correspondance entre outils. Nous nous intéressons dans la seconde partie de cette thèse à une formalisation dans un assistant à la preuve de l’introduction de composants dans un langage de modélisation et des liens avec les activités de validation et vérification. Le but est d’étudier la préservation des propriétés par composition : les activités de vérification sont généralement coûteuses en terme de temps et d’effort, les faire d’une façon compositionnelle est très avantageux. Nous partons de l’atelier formel pour l’Ingénierie Dirigée par les Modèles Coq4MDE. Nous suivons la même ligne directrice de développement prouvé pour formaliser des opérateurs de composition et étudier la conservation des propriétés par assemblage. Nous nous intéressons au typage puis à la conformité de modèles par rapport au métamodèle et nous vérifions que les opérateurs définis permettent de conserver ces propriétés. Nous nous focalisons sur l’étude d’opérateurs élémentaires que nous exploitons pour spécifier des opérateurs de plus haut niveau. Les préconditions des opérateurs représentent les activités de vérification non compositionnelles qui doivent être effectuées en plus de la vérification des composants pour assurer la postcondition des opérateurs qui est la propriété souhaitée. Nous concluons en présentant des perspectives pour une formalisation algébrique en théorie des catégories.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Laboratory name:
Research Director:
Pantel, Marc and Ait Ameur, Yamine
Statistics:download
Deposited On:04 Mar 2014 22:58

Repository Staff Only: item control page