Integrating Veri able Assume/Guarantee Contracts in UML/SysML

Abstract

The compositional approach based on components and driven by requirements is a common method used in the development of critical realtime embedded systems. Since the satisfaction of a requirement is subject to the composition of several components, de ning 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 speci cations 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 de ned 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 veri cation of requirement satisfaction and for their traceability.

Introduction

Nowadays critical real-time embedded systems grow larger in size and more complex. Their development is a challenging task and is often error-prone. A way for system designers to tackle this issue is to use a compositional approach driven by requirements. For example, process-oriented standards such as DO-178C [ 14 ] highlight the need to model requirements at di erent levels of abstractions during development and to ensure their traceability at each design iteration step.

However, requirements are often di cult to be mapped to components: several components combine together to satisfy a requirement and a component may be involved in the satisfaction of several requirements. In order to achieve provably correct compositional design, one needs a way to abstractly specify how a particular component K participates in ful lling a requirement '. Such a speci cation can take the form of a contract : a pair (assumption, guarantee) where the assumption is an abstraction of K's environment behavior and the guarantee is an abstraction of K's behavior given that the environment behaves according to the assumption. Such a contract can then be used to model the point of view of the component with respect to the requirement '. Contracts for reactive and real-time components have received a lot of attention from the research community recently, as discussed in x5.

Besides the important role contracts can play in system design, they can also be used as basic blocks for compositional veri cation of requirement satisfaction. In [ 11 ] we have introduced a contract-based theory for compositional veri cation of systems of communicating Timed Input/Output Automata (TIOA) with the intention to use it as underlying semantics for contract-based UML/SysML [ 19, 18 ] modeling and veri cation.

This paper complements the theory from [ 11 ] by extending UML/SysML with the language elements needed for modeling contracts and their relations. The paper is structured as follows: in x2 we summarize the contract-based reasoning theory we have de ned and we present the OMEGA UML/SysML pro le [ 8 ] on which we want to apply the formal theory. In x3 we propose a meta-model for the contract theory and a set of constraints and well-formedness rules needed to make the system model veri able with contracts. Then, an instantiation of the meta-model for the OMEGA UML/SysML pro le is discussed. x4 presents the application of our approach to an industry-grade system model, the ATV SGS case study previously described without contracts in [ 9 ], before concluding. 2 2.1

Background

Timed Input/Output Automata

Many mathematical formalisms have been proposed in the literature for modeling communicating timed reactive components. Our work is based on a variant of Timed Input/Output Automata of [ 13 ] since it is one of the most general formalisms, thoroughly de ned and for which several interesting compositionality results are already available. A TIOA speci es a state space and a set of admitted timed behaviors for a component. The parallel composition of TIOAs (denoted k in the following) is based on synchronization of corresponding inputs/outputs and the interleaving of other actions. The main di erences between our variant and that of [ 13 ] are that (1) matched input-outputs resulting from a composition of two automata result in a visible I/O action which is not involved in synchronizations thereafter (in [ 13 ] the result is an output, which is not consistent with the semantics of signals in UML or SysML) and (2) continuous variables are restricted to Alur-Dill-style linear clocks [ 1 ] in order to allow the use of known symbolic simulation and veri cation methods (unavailable for the more general model of [ 13 ]). For the full de nition of the formal model, the reader is referred to [ 11 ]. 2.2

A UML/SysML Pro le Based on Timed Input/Output Automata

In previous work [ 5 ] we have considered the high-level modeling of embedded realtime systems in UML/SysML with a semantics provided in terms of TIOA. The result of this work is a semantic pro le for UML and SysML called OMEGA and a set of tools for simulation and model-checking, the IFx-OMEGA toolset1.

In OMEGA, the architecture of a system is expressed in the usual way in UML (class diagrams) and in SysML (block de nition diagrams and internal block diagrams). Classes/blocks may use most of their features: properties (attributes and parts), signals receptions, interconnection elements (port, connector, interface) and relations (association, composition and generalization). The hierarchical architecture of components (and systems) is speci ed through composite structures.

The behavior of atomic components is modeled by state machines with standard UML actions on transitions. The operational semantics of each component instance is a timed input/output automaton. The TIOAs corresponding to components are composed in parallel and communicate by asynchronous signal exchanges. This imposes that all communications between objects/block instances are de ned as signal outputs and receptions that are transferred via ports and connectors. Ports need to be typed with interfaces that contain the list of signals transferred to or from the component's environment. With respect to the actions described on transitions, the semantics supports a signi cant part of the UML action meta-model, including signal output, assignment, expression valuation and control ow structuring statements. The translation between OMEGA modeling concepts and the underlying TIOA semantics is automatic in IFx-OMEGA.

1 http://www.irit.fr/ifx ⪯ C-1

G

A

φ A

G

Conformance :

A || G ⪯ φ C1

S

A1

G1 K1

C C3

A3

G3 K3

A2 K2

Dominance : {C1, C2, C3} dominates C G2

C2 Satisfaction :

Ki ⊧ Ci , ∀i bidirectional communication satisfaction

E

The temporal elements of TIOA, such as clocks, clock actions and timed guards actions have corresponding language constructs in the OMEGA pro le. The elapsing of time is constrained by transition urgency stereotypes inspired from timed automata with urgency [ 4 ]: time delay is blocked if one of the active transitions in the current state is stereotyped <eager >, it is upper-bounded if an active transition is stereotyped <delayable> and is unbounded otherwise (i.e., if all active transitions are stereotyped <lazy >, which is by default).

The pro le also proposes mechanisms for formalizing requirements, in particular in the form of real-time safety properties described by observer classes (identi ed by a stereotype <observer >). The state machine of these classes uses special primitives for monitoring the system state and events and gives verdicts about the (non-)satisfaction of a property by using labels (e.g., stereotype <error >) on states.

For a more complete description of the UML/SysML component model used in OMEGA and of the mapping of notions, the reader is referred to [ 17 ]. 2.3

A Theory of Contracts for Timed Input/Output Automata

In [ 11 ] we de ned a theory for modeling and reasoning with contracts for TIOA. The theory is an extension of a meta-theory de ned in [ 22, 21 ]. A contract for a TIOA component K is a pair of TIOAs that model the assumption (A) and the guarantee (G). The satisfaction of the contract is de ned formally by a relation based on trace inclusion between K k A and G k A modulo the set of actions that are of interest for the contract. The theory also provides the necessary mechanisms for compositional reasoning with contracts, explained in the following.

Consider that the objective is to prove that a system S composed of several components K1; K2; ; Kn satis es a property ' (see Fig. 1) under a certain hypothesis A on the behavior of its environment. The method consists in de ning a more abstract speci cation G of the system such that A k G satis es ' (conformance step in Fig. 1). Once this step performed, one will be inclined to verify that the system S satis es the contract C = (A; G). However, it is often impossible to verify directly (i.e. by checking trace set inclusion) that the composite system S satis es the contract because of the combinatorial explosion of the state space. To avoid this problem, the method de ned in [ 11, 21 ] uses a decomposition of the proof in independent steps based on the de nition of a set of individual contracts C1; C2::: for the components K1; K2:::, which, when put together, ensure the global contract C. We say that fC1; C2; g dominates C (dominance step in Fig. 1). The theory in [ 11, 21 ] provides a set of su cient conditions for dominance which can be checked independently with lesser combinatorial complexity. In addition to the conditions for dominance, one also has to check that each component Ki satis es the contract Ci (satisfaction step in Fig. 1). 3

Extending UML and SysML for Modeling Contracts

In this section we present the UML and SysML extensions that we propose in order to support modeling and reasoning with contracts. In x3.1 we describe a domain meta-model of the contract-related concepts which extends the UML meta-model. The adaptation for SysML is discussed brie y at the end, as is relatively straightforward. We then discuss in x3.2 the constraints and well-formedness rules imposed on the key notions in order to make models with contracts compliant with the theory from [ 11 ] and thus veri able. Finally, in x3.3 we discuss the mapping of the metamodel concepts as a UML/SysML pro le, using the standard extension mechanisms (stereotypes). 3.1

A Meta-Model for Contracts in UML

Within the contract theory we have presented there are two categories of concepts: (1) those related to contract modeling represented in the upper part of the metamodel given in Fig. 2 and (2) those related to modeling relations between contracts, used for example in veri cation, represented in the lower part of Fig. 2.

The requirement ' that the component model has to satisfy is represented by the meta-class SafetyProperty. This meta-class is left unspeci ed at this point since di erent formalisms could be used to model a requirement, such as temporal logics, automata-based languages, etc. In x3.3 we instantiate the meta-model in the OMEGA pro le, which uses an observer for modeling a SafetyProperty.

The assumption/guarantee of a contract is modeled by the corresponding metaclass Assumption/Guarantee type of Class. Each of these two elements is modeled by a class that has a behavior expressed by a state machine and communicates (only) through ports. Assumptions/guarantees are thus described in the same language as the system components. In order to have a clear semantics in terms of TIOA, they are subject to few restrictions: they should not be involved in associations, generalizations, realizations (except the interface realizations demanded by ports) and dependencies. An assumption or guarantee may de ne a composite sub-structure. Such an example is provided in the case study of x4.

A contract is represented by the meta-class Contract as a composite structure, containing exactly one assumption and one guarantee (i.e. any other properties are forbidden) and does not exhibit any behavior. The only relations a contract may be involved in are those that represent the veri cation relations used in our theory, as described below.

If a contract serves in the conformance step in the methodology depicted in Fig. 1, this is modeled using a Conformance relation (a kind of Dependency ) between the Contract and the corresponding SafetyProperty. One can use the same contract for several safety properties.

The dominance relation is represented by the meta-class Re nement type of Dependency. One contract is re ned by a set of contracts. Note that this is possible since UML de nes Dependency from n clients to n suppliers. To ensure that no cycles may be modeled, the following constraint is imposed: the target of a Re nement is not a member of the source set.

Finally, the relation between a component and the contract that it must satisfy is represented by two relations: one at the level of the type of the component and one at the level of the instance (the part which participates in a composite structure where the contract is relevant and which is modeled by the meta-class Property ). On the level of the type, an Implementation relation (a kind of Dependency ) between a class and a contract models the fact that the class satis es the contract. One class can satisfy several distinct contracts. On the level of instances, a ContractUse relation (also a kind of Dependency ) between a Property, which is part of a composite structure, and a Contract models the fact that the contract is used for veri cation within the context of that composite structure. A Property may use a contract if and only if its class implements that contract.

All constraints have been formalized with OCL [ 20 ]. Their code can be found in an extended version of this paper [ 10 ]. This meta-model can be easily adapted for the SysML language by de ning the meta-classes Contract, Assumption and Guarantee as extensions of the stereotype block applied on the meta-class Class from UML4SysML package. Similarly, the meta-class Dependency belongs to the same package. 3.2

Well-Formedness Rules for Veri able Contracts

In order to be able to apply the contract-based veri cation theory from [ 11 ] we need to make sure that the hypotheses and constraints imposed by the formal framework are satis ed by the system model. In the following we formalize these constraints at the meta-model level by a set of well-formedness rules.

Within the formal framework, a contract is modeled by a pair (A; G) of TIOA such that the set of inputs/outputs of G is a subset of the set of inputs/outputs of the component implementing the contract and the composition of A and G is a closed system. To ensure this, the set of ports of a Guarantee must correspond to a subset of the set of ports of the component for which the guarantee is de ned. The correspondence is based on the port name and the port type and direction must coincide. We consider that when a port is present in the guarantee, all the corresponding signal receptions de ned by the port type are handled in the guarantee. Moreover, as the composition between an Assumption and a Guarantee must be closed, every port of the Guarantee must have a corresponding conjugated port on the side of the Assumption, with the same type and reversed direction.

The dominance relation is also subject to the re nement of provided/required requests. This rule is also expressed with respect to ports: a port of the guarantee which is the target of the re nement must be matched (by name and type) by a port of one of the re ning guarantees and must not be matched by a corresponding conjugated port (i.e. with reversed directionality) of another from the re ning guarantees.

The theory from [ 11 ] also induces some constraints on the state machines of assumptions and guarantees. In particular, the behavior of an assumption or guarantee should not impose constraints on time progress. This is realized on the UML/SysML level ensuring that all transitions in these state machines are stereotyped <lazy > and that there is at most one output action on any transition.

Furthermore, for a model with contracts to be used in compositional veri cation according to the methodology described in x2, the model must describe a unique and complete proof tree: all implemented contracts are used within a context and for all SafetyProperty there is a contract conforming to it. The rules described above have been formalized in OCL and can be found in [ 10 ]. 3.3

Instantiating the Meta-Model in the OMEGA Pro le

In order to use contracts in a standard UML or SysML model, one needs to capture the information from the meta-model described in the previous section in the form of standard extensions, namely using stereotypes. Since all the new concepts introduced in the meta-model inherit from an existing meta-class (either Class or Dependency ), we choose to represent them as stereotypes of these base meta-classes. Thus, we use for the meta-class Class the stereotypes <contract >, <assumption>, <guarantee>, and <observer > (which already exists in OMEGA and is reused for representing SafetyProperty ). For contract relations, the stereotypes of Dependency that correspond to the meta-model elements are <contractImplementation>, <contractUse>, <contractRe nement > and <contractConformance>.

As explained before, from the semantic point of view, Contracts are not handled in the same way as usual classes/blocks as they are not considered executable elements of the system. Contracts are only used by the veri cation tools to check the validity of the conformance, dominance and satisfaction relations. The choice to describe contracts as classes is due to the fact that the syntax of contracts reuses much of the standard syntax of classes: we need to represent a contract as a closed composite structure with ports and links for the communication between the assumption and the guarantee and between the assumption and the component which uses the contract, interfaces to statically type the sets of inputs and outputs of each sub-component and behavior in the form of state machines. 4

The ATV Solar Generation System Case Study

The concepts and the reasoning method previously described have been applied on a case study, an industrial-grade system model of a subsystem of the Automated Transfer Vehicle (ATV). The ATV, developed by Astrium Space Transportation for the European Space Agency, is a spacecraft put into orbit by the European heavy launcher Ariane-5 with the aim of supplying the International Space Station. This case study consists of the Solar Wing Generation System (SGS) [ 9 ] responsible for the deployment and management of the solar wings of the vehicle. The SysML model used in the following, provided by Astrium Space Transportation, was obtained by reverse engineering the actual SGS system for the purpose of this study.

The SGS system model2 illustrated in Fig. 3 summarizes the three main components involved in the case study: the mission and vehicle management (MVM ) part that initiates SGS wing deployment, the SOFTWARE part of the SGS that based on requests received from the MVM executes the corresponding automated procedures and the HARDWARE part that models the four physical wings. The communication between components is realized via asynchronous signals transported through ports and connectors. Due to the large number of ports (661) and connectors (504), Fig. 3 presents a simpli ed architectural view of SGS and only shows a link between two parts where several connectors and ports are involved in the actual model. Let us mention that the veri cation steps presented below have been performed on the initial system model.

Under the hypothesis that at most one hardware failure may occur during a run, which is embedded in the HARDWARE model, the main goal of the case study is to verify the following property ': after 10 minutes from system start-up, all four wings are deployed.

Due to the size and the complexity of the model, applying model-checking directly leads to combinatorial explosion and the veri cation of ' does not nish. We explain in the following how the property ' was veri ed using the contract-based reasoning methodology. We start by modeling the property '. This implies identifying what the observer corresponding to the safety property ' must monitor. In our case, the block phi must observe the answer that each wing provides with respect to its status (deployed or not deployed) when interrogated by the software. So, the property ' expressed with respect to wing behavior must be satis ed by the HARDWARE block instance that contains them. With regard to Fig. 1, the HARDWARE is the subsystem S and WINGi, i = 1; 4, are the components Ki. The environment of the subsystem is given by the parts with which it communicates: bidirectional communication is directly established between SOFTWARE and HARDWARE, while SOFTWARE depends on the behavior of MVM. Thus, the environment E of Fig. 1 is represented here by the composition of MVM and SOFTWARE.

Next, we provide a contract C = (A; G) such that it conforms to '. In order to comply to the contract methodology, C is implemented by HARDWARE 's type and it is used by this part within the proof tree. We use as assumption A the concrete environment of HARDWARE, the composition between MVM and SOFTWARE itself, which thus satis es by construction the mirror contract C 1 = (G; A). Keeping this composition as assumption is not problematic since its state space has a manageable size. As guarantee G we use the following abstraction derived (manually) from the individual behavior of wings: for each wing status interrogation, the target wing answers either as not deployed for at most 400 seconds or as deployed after at least 130 seconds. In order to ensure that the contract de nes a closed system, since MVM kSOFTWARE sends all possible requests to HARDWARE, we equip G with all ports de ned by HARDWARE and we enrich the behavior of G to ignore all other requests. Then G and HARDWARE have the same set of ports: no re nement of requests is performed and the corresponding rule is satis ed.

The third step consists in modeling a set of contracts fC1; C2; C3; C4g that re ne C and proving that each contract Ci = (Ai; Gi) is implemented by WINGi 's type, i = 1; 4. The environment for WINGi is given by the environment of the subsystem HARDWARE and all WINGj, j 6= i. We use the following abstraction WAj for WINGj : the wing is either not deployed for at most 400 seconds or deployed from at least 130 seconds while all other received requests are consumed. The assumption Ai is the parallel composition of MVM, SOFTWARE and WAj, j 6= i. The guarantee Gi 2 The case study is represented using the notation conventions of IBM Rhapsody: http: //www-03.ibm.com/software/products/us/en/ratirhap/. 1 MVM:MVM 1 SOFTWARE:SOFTWARE

1 WING2:WING 1 HARDWARE:HARDWARE 1 WING1:WING «contractUse» «contractUse» 1 WING3:WING «contractUse» 1 WING4:WING «contractUse» «block,contract»

C1 «block,contract»

C2 «block,contract»

C3 «block,contract»

C4 «contractConformance» «block,observer»

phi «block,contract»

C «contractRefinement» «contractUse» is the projection of G on WINGi. Again the re nement of requests is not considered and since the ports of HARDWARE with respect to WINGi are identical to the ports of WINGi, both rules on port set inclusion for implementation and re nement are satis ed. Moreover, each Ci de nes a closed system.

After this step the proof obligation tree is complete. The veri cation involves 10 intermediate steps: 4 for verifying that each wing satis es its contract, 5 su cient conditions for dominance between fC1; C2; C3; C4g and C and one for proving that A k G '. Each veri cation step is performed by the OMEGA-IFx model checker in a few hours. The overall e ort of the building the contracts and performing the veri cation steps was of about 5 person*days. Even though the translation and veri cation algorithm are automated, two intermediate modeling steps - connecting assumptions to components via links and transforming the state machine of guarantees into observer (timed trace inclusion is veri ed using observers) - remain manual. The automation of these steps is currently under development. For further details on contract-based veri cation of the SGS case study, the reader is referred to [ 11 ]. 5

Related Work

Modeling and verifying contracts for components is a long line of research, whose origins date back to Hoare logic [ 12 ]. Syntactical and behavioral contracts, as classi ed in [ 3 ], have been explored for specifying composition constraints and pre/post conditions for operations and also for modeling transformation of models and execution semantics. Contracts as a language construct have emerged with the Ei el programming language [ 16 ] and have since been explored for various programming and speci cation models. In this section we concentrate on work aiming to introduce contracts in high-level modeling languages. For a discussion of more theoretical works on contracts and contract-based veri cation the reader is referred to [ 11 ].

Weis et al. [ 23 ] propose to model a contract for a component in UML by an interPage f1aocf1e and to specify its role: it can be either a required contract on which the component depends or a provided contract that is realized by the component. Syntactically, this representation of contracts is similar to ours: we also make the distinction between the required behavior of the environment and the provided behavior of the component by taking into account the assumption over the environment. However, our contracts are richer since they model a behavior that can be used for component validation, while the contracts of [ 23 ] can be used only for composability checking during the development phases.

The Kmelia component model [ 15, 2 ], based on the work described above, provides means to verify the functional correctness of behavioral contracts for services: the behavior of an operation is modeled as a Labeled Transition System and formal veri cation can be realized within di erent tools via model transformation. Their meta-model de nes for a contract the source implementing it as an aggregated element (operation or interface) and models explicitly the contract satisfaction results. But this formalism does not describe how the order in which services are called by and from a component can be veri ed, order that can be seen similar to our state machines from components. Furthermore, it does not provide a connection to high-level modeling languages as UML/SysML.

Contracts modeled as pre/post conditions are used in [ 7 ] for the veri cation of model transformation: the assumption is represented by an OCL constraint on the source model and the guarantee is an OCL constraint on the target model. Moreover, with respect to the syntax of contracts the two approaches are di erent: while the one we describe considers contracts only for components, [ 7 ] models contracts for all model elements. The same contracts are used in [ 6 ] to model the execution semantics of UML elements which is seen as a particular case of model transformation.

To the best of our knowledge, this study is the rst to consider behavioral contracts at the component level in UML/SysML and to provide veri cation relations for property satisfaction by contract-based reasoning. The meta-model we propose is generic enough to represent all the other meta-models previously described, excepting the veri cation results extension that is based on the dynamical execution of the model. 6

Conclusion

Based on a theory of contracts and on a methodological approach for reasoning with contracts introduced in previous work [ 11 ], we have proposed an extension of UML/SysML allowing to model contracts and use them for compositional veri cation of requirements. The extension is de ned as a meta-model, enriched with constraints and well-formedness rules to make contracts veri able. We have instantiated the extension within the OMEGA UML/SysML pro le to make it usable with standard model editors. The veri cation method is supported by the OMEGA-IFx toolset and the approach was validated on an industrial-grade system model.

Although an automatic model transformation from OMEGA system models to the input language of the IFx Toolset is already available, some of the steps for generating the intermediate contract-based veri cation models remain manual. Future work consists in automating all the intermediate model generation steps and in adding functionality for managing the proof obligations and results and for enforcing the rigorous veri cation methodology described in x2.3.

The method described before does not explicitly prescribe how to derive contracts for the whole system and for its components. In the case study described in x4, this task was relatively straightforward: since we make no additional assumption (A) about the environment, G is roughly the same as ', and the component guarantees are a projection of the desired global guarantee. There may be cases where the de nition of contracts is less obvious and the overhead is signi cant, and previous attempts to introduce contracts in programming have not enjoyed a widespread success due to this kind of overhead. Nevertheless, we believe that the case for contracts in early phases of system engineering is di erent than the case for software programming, and the overhead should be acceptable for certain critical systems. Further work is needed in order to lower the overhead by nding methods or methodological guidelines for deriving intermediate contracts from the properties one is trying to prove.

References

[1] R. Alur and D. L. Dill . A theory of timed automata . Theoretical computer science , 126 ( 2 ): 183 { 235 , 1994 .

[2] P. Andre , A. Gilles , and M. Messabihi . Veri cation de contrats logiciels a l'aide de transformations de modeles. In 7emes journees sur l'Ingenierie Dirigee par les Modeles (IDM) 2011 , 2011 .

[3] A. Beugnard , J.-M. Jezequel , N. Plouzeau , and D. Watkins . Making Components Contract Aware. Computer , 32 ( 7 ): 38 { 45 , July 1999 .

[4] S. Bornot and J. Sifakis . An algebraic framework for urgency . Information and Computation , 163 , 2000 .

[5] M. Bozga , S. Graf , I. Ober , I. Ober , and J. Sifakis . The IF Toolset . In Formal Methods for the Design of Real-Time Systems , volume 3185 of LNCS , pages 237 { 267 . Springer, 2004 .

[6] E. Cariou , C. Ballagny , A. Feugas , and F. Barbier . Contracts for model execution veri cation . In 7th European conference on Modelling foundations and applications (ECMFA) 2011 , pages 3 { 18. Springer, 2011 .

[7] E. Cariou , N. Belloir , F. Barbier , and N. Djemam . OCL contracts for the veri cation of model transformations . ECEASST , 24 , 2009 .

[8] E. Conquet , F.-X. Dormoy , I. Dragomir, S. Graf , D. Lesens , P. Nienaltowski , and I. Ober . Formal Model Driven Engineering for Space Onboard Software . In 6th International Symposium on Embedded Real Time Software and Systems (ERTS2 ) 2012 . Online website, 2012 .

[9] I. Dragomir , I. Ober , and D. Lesens . A case study in formal system engineering with SysML . In 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) 2012 , pages 189 { 198 . IEEE Computer Society, 2012 .

[10] I. Dragomir , I. Ober , and C. Percebois . Integrating veri able Assume/Guarantee contracts in UML/SysML . Technical report , IRIT, july 2013 . Available at http://www.irit.fr/~Iulian.Ober/docs/TR-Syntax.pdf.

[11] I. Dragomir , I. Ober , and C. Percebois . Safety Contracts for Timed Reactive Components in SysML . Technical report , IRIT, june 2013 . Submitted for publication . Available at http://www.irit.fr/~Iulian.Ober/docs/TR-Contracts.pdf.

[12] C. A. R. Hoare . An Axiomatic Basis for Computer Programming . Commun. ACM , 12 ( 10 ): 576 { 580 , 1969 .

[13] D. K. Kaynar , N. Lynch , R. Segala , and F. Vaandrager . The Theory of Timed I/O Automata - Second Edition . Morgan & Claypool Publishers, 2010 .

[14] RTCA Inc . Software Considerations in Airborne Systems and Equipment Certi cation . Document RTCA/DO-178C , 2011 .

[15] M. Messabihi , P. Andre , and C. Attiogbe . Multilevel Contracts for Trusted Components . In International Workshop on Component and Service Interoperability , volume 37 of EPTCS , pages 71 { 85 , 2010 .

[16] B. Meyer . Applying Design by Contract . Computer , 25 ( 10 ): 40 { 51 , Oct . 1992 .

[17] I. Ober and I. Dragomir. OMEGA2: A New Version of the Pro le and the Tools . In 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) 2010 , pages 373 { 378 . IEEE Computer Society, 2010 .

[18] Object Management Group. Systems Modelling Language (SysML) v1.1 , 2008 .

[19] Object Management Group. Uni ed Modelling Language (UML) v2.2 , 2009 .

[20] Object Management Group. Object Constraint Language (OCL) v2.2 , 2010 .

[21] S. Quinton . Design, veri cation et implementation de systemes a composants . PhD thesis , Universite de Grenoble, 2011 .

[22] S. Quinton and S. Graf . Contract-based veri cation of hierarchical systems of components . In Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM) 2008 , pages 377 { 381 , 2008 .

[23] T. Weis , C. Becker , K. Geihs , and N. Plouzeau . A UML Meta-model for Contract Aware Components . In 4th International Conference on The Uni ed Modeling Language, Modeling Languages, Concepts , and Tools (UML) 2001 , pages 442 { 456 . Springer, 2001 .