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

The composition of two MIODs S and T synchronizes transitions whose labels
refer to shared operations. For instance, a transition with label [ ϕ S ]? op [ π S ]of
S is synchronized with a transition with label [ ϕ T ]! op [ π T ]of T which results
in a transition with label [ ϕ S ∧

π T ] where the original preconditions
(postconditions resp.) are combined by logical conjunction. Transitions whose la-
bels concern shared operations which cannot be synchronized are dropped while
all other transitions are interleaved in the composition. Concerning modalities
we follow the MIO composition operator which yields a must-transition if two
must-transitions are synchronized and a may-transition otherwise.

ϕ T ] op [ π S ∧

Definition 7 (Composition of MIODs). The composition of two composable
MIODs S and T is the MIOD

Σ T ,Δ may

S ⊗ T =( states S ×

states T , ( start S , start T ) ,Σ S ⊗

T ,Δ must S⊗T ) S ⊗

where the transition relations Δ may
S⊗T

and Δ must
S⊗T

are defined by the following rules:

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

( s, [ ϕ S ] op [ π S ] ,s )

∈ ∈

op ∈ sh ( O S , O T ) ,

Δ S⊗T

γ ∈{ may , must }

(( s, t ) , [ ϕ S ∧ ϕ T ] op [ π S ∧ π T ] , ( s ,t )) ∈

Δ S , ( s, [ ϕ S ] op [ π S ] ,s )

∈ t ∈ states T

op ∈ sh ( O S , O T ) , γ ∈{ may , must }

Δ S⊗T (( s, t ) , [ ϕ S ] op [ π S ] , ( s ,t )) ∈

Δ T ,

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

∈ s ∈ states S

op ∈ sh ( O S , O T ) , γ ∈{ may , must }

Δ S⊗T (( s, t ) , [ ϕ T ] op [ π T ] , ( s, t )) ∈

Example 6. Assume given the MIOD S Leg of Fig. 1 and a MIOD S LegC describing
the behavior of the controller component LegC . Fig. 3 shows the result of the
synchronization of the two transitions of S LegC and S Leg

concerning the shared

[ a =min( distance − gone, maxStep )]

! swing ( a )

[ currStep ≤ a ]

S LegC s C s C

[ a ≤ maxStep + maxStep/ 10]

? swing ( a )
[ currStep = a ∧ steps = steps +1]

S Leg s L

s L

[( a =min( distance − gone, maxStep )) ∧ ( a ≤ maxStep + maxStep/ 10)]

swing ( a )

[ currStep = a ∧ steps = steps +1]

s C ,s L s C ,s L

S LegC ⊗ S Leg

Fig. 3. MIOD composition