Harnessing rCOS for Tool Support—The CoCoME Experience - Formal Methods and Hybrid Real-Time Systems - page 90

1. Init 2 ⇒ ( Init 1 ; ρ )
2. ρ ⇒ ( guard 1 ( op )= guard 2 ( op )) for all op ∈ MDec 1 .
3. for each op ∈ MDec 1 , MSpec 1 ( op ); ρ ρ ; MSpec 2 ( op )
Similarly, contract refinement can also be proved by a surjective upward
simulation [6].
Theorem 3 (Completeness of Simulations)
If Ctr 1 Ctr 2 ,thereexistsa Ctr such that
Ctr 1 up Ctr Ctr 2

up and down denote upwards and downwards simulations, respectively.

down Ctr 2 Ctr 1 Ctr

Components. A component is an implementation of a contract. Formally
speaking, a component is tuple C =( I, Init, MCode, PriMDec, PriMCode, InMDec ) ,
where
- MCode and PriMCode map a public method to a private method m to a
guarded command g m → c m ,
- InMDec is the set of required methods in the code, called required interface .
The semantics [[ C ]] is a function that calculates a contract for the provided in-
terface for any given contract InCtr of the required interface
[[ C ]] ( InCtr ) def =(( I, MSpec ) , Init, PriMDec, PriMSpec )

where the specification is calculated from the semantics of the code, following
the calculus established in UTP.
Acomponent C 1 is refined by another component C 2 , denoted by C 1 C 2 if
1. the later provides the same services as the former, C 1 .MDec = C 2 .MDec
2. the later requires the same services as the former C 1 .InMDec = C 2 .InMDec ,
and
3. for any given contract of the required interface, the resulting provided con-
tract of the later is a refinement of that of the former, C 1 ( InCtr ) C 2 ( InCtr ) ,
holds for all input contracts InCtr .
Note that the notion of component refinement is used for both component cor-
rectness by design and component substitutability in maintenance. One of the
major objectives of rCOS is to prove design patterns as refinement rules, and
automate refinement rules as model transformations . We hope this will help to
reduce the amount of verification required.

Simple Connectors. To support the development activity, the semantic frame-
work also needs to define operators for connecting components, resulting in
new contracts, constructs for defining glue processes, and constructs for defin-
ing processes. In summary, the framework should be compositional and support
both functional and behavioral specification . In rCOS, simple connectors between
components are defined as component compositions. These include plugging (or
union ), service hiding , service renaming ,and feedback . These compositions are
shown in Figs. 2-4.