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

Example 7. In S LegC ⊗ S Leg ,thestate( s C ,s L ) is a reachable state, see Fig. 3.

Compatibility holds because for the operation call swing ( a ) issued by S LegC
in state s C there exists a single must-transition of S Leg which guarantees the
reception of swing ( a ) in state s L such that the following holds (for any usual
satisfaction relation):

( a =min( distance − gone , maxStep )) ⇒ ( a ≤ maxStep + maxStep / 10),

( currStep = a steps = steps +1) ( currStep ≤

∧ ⇒ a ).

We are now able to state our central result which says that compatibility is
preserved by refinement and that refinement is compositional (for compatible
MIODs). Thus our framework supports independent implementability.

Theorem 1 (Independent Implementability). Let S , S , T ,and T be
MIODs, and assume that S , T as well as S , T are composable. If S

∼ T ,

S ≤ m S and T ≤ m T ,then S ∼ T and S ⊗ T ≤ m S ⊗ T .

Proof. We first prove preservation of compatibility. Let ( s ,t ) ( S ⊗ T )be

∈R

a reachable state in S ⊗ T . It follows from condition 2 of Def. 3 that there

exists a reachable state ( s, t ) T ) such that t ≤ m t and s ≤ m s .

Assume that there exists a transition ( s , [ ϕ S ] op [ π S ] , s )

∈R ( S ⊗

Δ may
S

∈ such that op ∈

O req

S ∩O prov

Δ may
S

.From s ≤ m s it follows that there exists ( s, [ ϕ S ] op [ π S ] , s )

∈

T

such that ϕ S ⇐ ϕ S and π S ⇒ π S .From S ∼ T it follows that there exists

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

T

ϕ T .Since t ≤ m t we can conclude ∈ such that ϕ S ⇒

that there exists ( t , [ ϕ T ] op [ π T ] , t ) Δ must

T

∈ such that ϕ T ⇒ ϕ T . It follows

that ϕ T . Then, we must additionally show that for all accepting may-

transitions of T , the postcondition matches π S which is again straightforward.
For the proof of compositionality of modal refinement we define

ϕ S ⇒

≤ m ⊆

( states S

× states T ) × ( states S × states T )by

( s ,t )

≤ m ( s, t )iff s ≤ m s, t ≤ m t, ( s ,t ) ∈R

( S ⊗

T )and( s, t ) ∈R

( S

⊗ T ) .

≤ m ( start S , start T ) and it remains to show that ≤ m Obviously, ( start S , start T )

is a modal refinement between the states of S ⊗ T and the states of S

⊗ T .The

detailed proof can be found in [2].

Example 8. In Fig. 4, the principle of independent implementability is illustrated
in terms of our running example showing small excerpts of four MIODs. Starting
from the abstract MIODs T LegC and T Leg we first check their compatibility, i.e.

T LegC ∼ T Leg . Then we refine T LegC

and T Leg

independently of each other by

the MIODs S LegC and S Leg , respectively. Thm. 1 guarantees, first, that S LegC

and S Leg are compatible (as explained explicitly in Ex. 7) and secondly, that

S LegC ⊗ S Leg ≤ m T LegC ⊗ T Leg holds.