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

[ true ]? swing ( a )[ currStep ≤ a ]

[ a ≤ maxStep ]

! swing ( a )

t L

t L

[ currStep ≤ a ]

t C

t C

[ a ≤ maxStep ]? swing ( a )[ currStep = a ]

T ∼ T LegC Leg

S ∼ S LegC Leg

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

! swing ( a ) ? swing ( a )

[ currStep ≤ a ] [ currStep = a ∧ steps = steps +1]

s C s L s C s L

Fig. 4. Compositional refinement of compatible components LegC and Leg

5Con lu on

Modal I/O-transition systems (MIOs) provide a flexible framework for the spec-
ification and refinement of interacting, concurrent components. In this work we
have extended MIOs to take into account data constraints which allow to specify
the behavior of components with regard to changing data states. We have shown
that our proposal satisfies the requirements of an interface theory guaranteeing
preservation of compatibility and compositionality of refinements when moving
from abstract to more concrete specifications of interacting components.
We have tried to keep the formalism for refinement as simple as possible at
the cost of some restrictions. For instance, one would like to be able to refine
a single (abstract) must-transition with some precondition ϕ by several (con-
crete) transitions which distribute the precondition over several cases ϕ i for

i =1 ,...,n , such that ϕ ⇒ i ϕ i . Similarly, one could relax the requirements
for may-transitions. Moreover, it would not be a problem to integrate state in-
variants in our framework.
In this paper we have worked on the level of specifications and their refinement
and compatibility which are clearly dependent on the syntactical representation
of the specification. We have not yet provided a formal semantics which would
allow us to define semantic notions of refinement and compatibility. A formal
semantics could be delivered in terms of the class of all correct implementations
of a specification as done for MIOs in [10] and for behavior protocols without
modalities but with data states in [3]. An implementation would then be mod-
eled by a transition system with must-transitions only and with concrete data
states given by valuations of the state variables. Concerning the interpretation of