Contract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to repartition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient.
Coherent extension, composition, and merging operators in contract models for system design / Passerone, R.; Incer Romeo, I.; Sangiovanni-Vincentelli, A. L.. - In: ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS. - ISSN 1539-9087. - 18:5s(2019), pp. 86.1-86.23. [10.1145/3358216]
Coherent extension, composition, and merging operators in contract models for system design
Passerone R.;
2019-01-01
Abstract
Contract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to repartition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient.File | Dimensione | Formato | |
---|---|---|---|
PasseroneRomeoASV19TECS.pdf
Solo gestori archivio
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
558.48 kB
Formato
Adobe PDF
|
558.48 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione