Contracts for Systems Design: Methodology and Application cases

Abstract : Recently, contract based design has been proposed as an ”orthogonal” approach that can be applied to all methodologies proposed so far to cope with the complexity of system design. Contract based design provides a rigorous scaffolding for verification, analysis and abstraction/refinement. Companion report RR-8759 proposes a unified treatment of the topic that can help in putting contract-based design in perspective. This paper complements RR-8759 by further discussing methodological aspects of system design with contracts in perspective and presenting two application cases. The first application case illustrates the use of contracts in requirement engineering, an area of system design where formal methods were scarcely considered, yet are stringently needed. We focus in particular to the critical design step by which sub-contracts are generated for suppliers from a set of different viewpoints (specified as contracts) on the global system. We also discuss important issues regarding certification in requirement engineering, such as consistency, compatibility, and completeness of requirements. The second example is developed in the context of the Autosar methodology now widely advocated in the automotive sector. We propose a contract framework to support schedulability analysis, a key step in Autosar methodology. Our aim differs from the many proposals for compositional schedulability analysis in that we aim at defining sub-contracts for suppliers, not just performing the analysis by parts—we know from companion paper RR-8759 that sub-contracting to suppliers differs from a compositional analysis entirely performed by the OEM. We observe that the methodology advocated by Autosar is in contradiction with contract based design in that some recommended design steps cannot be refinements. We show how to circumvent this difficulty by precisely bounding the risk at system integration phase. Another feature of this application case is the combination of manual reasoning for local properties and use of the formal contract algebra to lift a collection of local checks to a system wide analysis.
Type de document :
Rapport
[Research Report] RR-8760, Inria Rennes Bretagne Atlantique; INRIA. 2015, pp.63
Liste complète des métadonnées

Littérature citée [48 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01178469
Contributeur : Albert Benveniste <>
Soumis le : lundi 20 juillet 2015 - 10:49:20
Dernière modification le : vendredi 16 novembre 2018 - 01:40:17
Document(s) archivé(s) le : mercredi 21 octobre 2015 - 17:12:11

Fichier

RR-8760.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01178469, version 1

Citation

Albert Benveniste, Benoît Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for Systems Design: Methodology and Application cases. [Research Report] RR-8760, Inria Rennes Bretagne Atlantique; INRIA. 2015, pp.63. 〈hal-01178469〉

Partager

Métriques

Consultations de la notice

2499

Téléchargements de fichiers

609