• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 1
  • Tagged with
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Construction Incrémentale de Spécifications de Systèmes Critiques intégrant des Procédures de Vérification

Luong, Hong-Viet 01 October 2010 (has links) (PDF)
Cette thèse porte sur l'aide à la construction de machines d'états UML de systèmes réactifs. Elle vise à définir un cadre théorique et pragmatique pour mettre en oeuvre une approche incrémentale caractérisée par une succession de phases de construction, évaluation et correction de modèles. Ce cadre offre des moyens de vérifier si un nouveau modèle est conforme à ceux définis durant les étapes précédentes sans avoir à demander une description explicite des propriétés à vérifier. Afin de pouvoir analyser les machines d'états, nous leur associons une sémantique LTS ce qui nous a conduit à définir une procédure de transformation automatique de machines d'états en LTS. Dans un premier temps, nous avons défini et implanté des techniques de vérification de relations de conformité de LTS (red, ext, conf, et confrestr). Dans un second temps, nous nous sommes intéressés à la définition d'un cadre de construction incrémentale dans lequel plusieurs stratégies de développement peuvent être mises en \oe uvre en s'assurant que le modèle final élaboré sera une implantation conforme à la spécification initiale. Ces stratégies reposent sur des combinaisons de raffinements qui peuvent être de deux types : le raffinement vertical pour éliminer l'indéterminisme et ajouter des détails ; le raffinement horizontal pour ajouter de nouvelles fonctionnalités sans ajouter d'indéterminisme. Enfin, nous transposons la problématique de construction incrémentale d'une machine d'états à la construction d'architectures dont les composants sont des machines d'états. Des conditions sont définies pour assurer la conformité entre des architectures dans le cas de la substitution de composants.

Page generated in 0.0818 seconds