Contract-Based Requirement Modularization via Synthesis of Correct Decompositions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theory of Computing Systems Année : 2016

Contract-Based Requirement Modularization via Synthesis of Correct Decompositions

Résumé

In distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a contract, given the satisfaction of smaller properties also represented as contracts. When the verification result is negative, designers must face the issue of refining the subproperties and components. This is an instance of the classical synthesis problems: " can we construct a model that satisfies some given specification? " In this work, we propose two strategies enabling designers to synthesize or refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraic method and show how it can be applied in different contract models to support top-down component-based development of distributed systems.
Fichier principal
Vignette du fichier
j52.pdf (586.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01406481 , version 1 (07-12-2016)

Identifiants

Citer

Thi Thieu Hoa Le, Roberto Passerone, Uli Fahrenberg, Axel Legay. Contract-Based Requirement Modularization via Synthesis of Correct Decompositions. Theory of Computing Systems, 2016, 15, ⟨10.1145/2885752⟩. ⟨hal-01406481⟩
287 Consultations
224 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More