Contracts for Systems Design: Methodology and Application cases
Albert Benveniste, Benoı̂t Caillaud, Dejan Ničković, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto Luigi Sangiovanni-Vincentelli, Werner Damm, Tom Henzinger, Kim G. Larsen · HAL (Le Centre pour la Communication Scientifique Directe) · 2015
Recently, contract based design has been proposed as an ”orthogonal” approach that can beapplied to all methodologies proposed so far to cope with the complexity of system design. Contract baseddesign provides a rigorous scaffolding for verification, analysis and abstraction/refinement. Companionreport 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 withcontracts in perspective and presenting two application cases.The first application case illustrates the use of contracts in requirement engineering, an area of system designwhere formal methods were scarcely considered, yet are stringently needed. We focus in particular to thecritical 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 inrequirement engineering, such as consistency, compatibility, and completeness of requirements.The second example is developed in the context of the Autosar methodology now widely advocated inthe automotive sector. We propose a contract framework to support schedulability analysis, a key step inAutosar methodology. Our aim differs from the many proposals for compositional schedulability analysisin that we aim at defining sub-contracts for suppliers, not just performing the analysis by parts—we knowfrom companion paper RR-8759 that sub-contracting to suppliers differs from a compositional analysis entirelyperformed by the OEM. We observe that the methodology advocated by Autosar is in contradiction withcontract based design in that some recommended design steps cannot be refinements. We show how tocircumvent this difficulty by precisely bounding the risk at system integration phase. Another feature ofthis application case is the combination of manual reasoning for local properties and use of the formalcontract algebra to lift a collection of local checks to a system wide analysis.