Safety Contracts for Timed Reactive Components in SysML

A variety of system design and architecture description languages, such as SysML, UML or AADL, allows the decomposition of complex system de-signs into communicating timed components. In this paper we consider the contract-based specification of such components. A contract is a pair formed of an assumption, which is an abstraction of the component’s environment, and a guarantee, which is an abstraction of the component’s behavior given that the environment behaves according to the assumption. Thus, a contract concentrates on a specific aspect of the component’s functionality and on a subset of its interface, which makes it relatively simpler to specify. Con-tracts may be used as an aid for hierarchical decomposition during design or for verification of properties of composites. This paper defines contracts for components formalized as a variant of timed input/output automata, in-troduces compositional results allowing to reason with contracts and shows how contracts can be used in a high-level modeling language (SysML) fo