OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Integrating verifiable Assume/Guarantee contracts in UML/SysML

Dragomir, Iulia and Ober, Iulian and Percebois, Christian Integrating verifiable Assume/Guarantee contracts in UML/SysML. (2013) In: International Workshop on Model Based Architecting and Construction of Embedded Systems - ACESMB 2013, 29 September 2013 - 29 September 2013 (Miami, United States).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
383kB

Abstract

The compositional approach based on components and driven by requirements is a common method used in the development of critical real-time embedded systems. Since the satisfaction of a requirement is subject to the composition of several components, defining abstract and partial behaviors for components with respect to the point of view of the requirement allows for a manageable design of systems. In this paper we consider such specifications in the form of contracts. A contract for a component is a pair (assumption, guarantee) where the assumption is an abstraction of the component's environment behavior and the guarantee is an abstraction of the component's behavior given that the environment behaves like the assumption. In previous work we have defined a formal contract-based theory for Timed Input/Output Automata with the aim of using it to express the semantics of UML/SysML models. In this paper we propose an extension of the UML/SysML language with a syntax and semantics for contracts and for the relations they must satisfy. Besides the important role that contracts have in design, they can also be used for the verification of requirement satisfaction and for their traceability.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Ceur-ws editor. The definitive version is available at http://ceur-ws.org/Vol-1084/
HAL Id:hal-01142471
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:15 Apr 2015 10:28

Repository Staff Only: item control page