Integrating Verifiable Assume/Guarantee Contracts in UML/SysML
Iulia Dragomir, Iulian Ober, Christian Percebois · 2013
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 en-vironment 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 sat-isfy. Besides the important role that contracts have in design, they can also be used for the verification of requirement satisfaction and for their traceability. 1