Une méthodologie de spécification et de validation de systèmes hétérogènes fondée sur un modèle de contrats pour la conception des systèmes embarqués

• Main Author: Glouche, Yann
• Language: FRE
• Published: Université Rennes 1 2009
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; contrat; hypothèse/garantie; langage synchrone; algèbre booléenne; langage de modules; système embarqué
• Online Access: http://tel.archives-ouvertes.fr/tel-00460260; http://tel.archives-ouvertes.fr/docs/00/46/02/60/PDF/these.pdf

Les contrats basés sur les notions d'hypothèses/garanties constituent un paradigme expressif pour une conception modulaire et compositionnelle de spécification de programmes. Ils sont devenus un concept fondamental dans les procédés employés par les outils de conception assistée par ordinateur, pour la conception de systèmes informatiques. Dans cette thèse, nous élaborons des fondements pour la mise en oeuvre de systèmes embarqués basée sur la notion de contrats. Nous proposons ainsi une algèbre de contrats basée sur deux concepts simples : les hypothèses et les garanties des composants sont définies par des filtres, les filtres sont caractérisés par une structure d'algèbre booléenne. Les choix effectués pour définir la structure des filtres permettent de définir une algèbre de Heyting sur l'ensemble des contrats. Un cadre de travail est ainsi défini, dans lequel les contrats sont utilisés pour vérifier la correction des hypothèses faites sur le contexte d'utilisation d'un composant, et pour fournir à l'environnement les garanties qui lui sont demandées. Nous utilisons cette algèbre pour définir un système de modules dont le paradigme de typage est basé sur la notion de contrats. Le type d'un module est un contrat caractérisé par les hypothèses faites par l'environnement et les garanties offertes par les comportements du module. Nous illustrons cette présentation avec la spécification d'un moteur à quatre temps.