Contribution à une démarche de vérification formelle d'architectures logicielles

Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles : DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que : les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00182871
Date25 October 2007
CreatorsGraiet, Mohamed
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0021 seconds