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
Résumé
Contract-based design is an expressive paradigm for a modular and compositional specification of programs. It is in turn becoming a fundamental concept in mainstream industrial computer-aided design tools for embedded system design. In this thesis, we elaborate new foundations for contract-based embedded system design by proposing a general-purpose algebra of assume/guarantee contracts based on two simple concepts: first, the assumption or guarantee of a component is defined as a filter and, second, filters enjoy the structure of a Boolean algebra. This yields a structure of contracts that is a Heyting algebra. In this framework, contracts are used to negotiate the correctness of assumptions made on the definition of a component at the point where it is used and provides guarantees to its environment. We put this algebra to work for the definition of a general purpose module system whose typing paradigm is based on the notion of contract. The type of a module is a contract holding assumptions made and guarantees offered by its behaviors. We illustrate this presentation with the specification of a simplified 4-stroke engine model.
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.