A Modal Interface Theory with Data Constraints - Formal Methods: Foundations and Applications - page 92

operation swing ( a ) which is an internal operation in the composition S LegC ⊗
S Leg . Similarly the shared state variable maxStep is an internal state variable in
S LegC ⊗

S Leg .

As discussed above, if we want to compose two MIODs it is first necessary
to check composability which is a purely syntactic condition. But then it is
of course important that the two components work properly together, i.e. are
behaviorally compatible. The following compatibility notion builds upon (strong)
modal compatibility of MIOs as defined in [4]. From the control point of view
(strong) compatibility requires that in any reachable state of the product S T

of two MIODs S and T ,ifoneMIOD may issue an output (in its current control
state) then the other MIOD is in a control state where it must be able to take
the corresponding input 3 . In the context of data states we have the additional
requirement that the data constraints of the two MIODs S and T must be
compatible. Since the data constraints imposed by a MIOD can be considered
as a contract (see Table 1) the two contracts according to S and T must match.
More precisely, matching means that the mutual assumptions and guarantees
of the two MIODs imply each other for any shared operation as illustrated in
Table 2. Thus, by combining the control flow and the data state aspects of
compatibility we obtain the following compatibility notion for MIODs.

⊗

Table 2. Data compatibility of MIODs

S T S ∼ T

[ ϕ S ]? m [ π S ] [ ϕ T ]!m[ π T ]

assume ϕ S guarantee ϕ T ϕ S ⇐ ϕ T

π S π T π S ⇒ π T

guarantee assume

[ ϕ S ]! n [ π S ] [ ϕ T ]?m[ π T ]

guarantee ϕ S assume ϕ T ϕ S ⇒ ϕ T

assume π S guarantee π T π S ⇐ π T

Definition 8 (Compatibility of MIODs). Let S and T be two composable
MIODs. S and T are compatible , denoted by S

∼ T , if for all reachable states

( s, t ) ∈R ( S ⊗ T ) ,

Δ may
S

O req
S

∩O prov
T

1. if ( s, [ ϕ S ] op [ π S ] ,s )

∈ and op ∈ ( ) , then there exists a

must-transition ( t, [ ϕ T ] op [ π T ] ,t ) Δ must

T

∈ such that ϕ S ⇒ ϕ T ,andforall

Δ may
T

may-transitions ( t, [ ϕ T ] op [ π T ] ,t ) ∈ it holds that π S ⇐ π T ;

Δ may
T

O req
T

∩O prov
S

2. if ( t, [ ϕ T ] op [ π T ] ,t )

∈ ∈

and op ( ) , then there exists a

must-transition ( s, [ ϕ S ] op [ π S ] ,s )

∈ Δ must

S

ϕ T ⇒ ϕ S ,andforall

such that

Δ may
S

may-transitions ( s, [ ϕ S ] op [ π S ] ,s ) ∈ it holds that π T ⇐ π S .

3 This concept follows a “pessimistic” approach where two components should be
compatible in any environment, in contrast to the “optimistic” approach pursued
in [6,9] which relies on the existence of a “helpful” environment.