OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Safety contracts for timed reactive components

Dragomir, Iulia and Ober, Iulian and Percebois, Christian Safety contracts for timed reactive components. (2014) In: International Conference on Current Trends in Theory and Practice of Computer Science - SOFSEM 2014, 25 January 2014 - 30 January 2014 (Nový Smokovec, Slovakia).

(Document in English)

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

Official URL: http://dx.doi.org/10.1007/978-3-319-04298-5_19


A variety of system design and architecture description languages, such as SysML, UML or AADL, allows the decomposition of complex system designs 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. Contracts 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, introduces compositional results allowing to reason with contracts and shows how contracts can be used in a high-level modeling language (SysML) for specification and verification, based on an example extracted from a real-life system.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. The definitive version is available at http://link.springer.com/chapter/10.1007%2F978-3-319-04298-5_19
HAL Id:hal-01147265
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:27 Mar 2015 08:37

Repository Staff Only: item control page