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 de systèmes embarqués
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
Contract-based design is an expressive paradigm for a modular and compositional specification of programs. 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. We illustrate this presentation with the specification of a simplified 4-stroke engine model.
Abstract FR:
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. 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 illustrons cette présentation avec la spécification d'un moteur à quatre temps.