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

of different types of state variables (provided, required and internal) which, in our
case, is a methodologically important ingredient to express the contract principle
between interface specifications. In our previous work, we have proposed in [3]
a formal semantics of behavior protocols based on model classes, but [3] does
not consider modalities and a refinement notion between specifications. On the
other hand, we have investigated in [4] various kinds of modal interface theories
with refinements but without taking into account constraints on data states.

Outline. The paper is organized as follows. In Sect. 2 we introduce modal I/O-
transition systems with data constraints (MIODs). Their refinement is consid-
ered in Sect. 3, and in Sect. 4 the composition and the compatibility of MIODs
is defined. Moreover, we show in Sect. 4 that our framework satisfies the re-
quirements of an interface theory concerning compositionality of refinement and
preservation of compatibility by refinement. In Sect. 5 we finish with some con-
cluding remarks.

Example 1. We use a hexapod robot as a running example. This insect-like, six-
leg robot exhibits a non-trivial control-flow behavior with a significant impact
of data states. When specifying such a complex subject, non-trivial synchroniza-
tion and coordination problems arise which must be addressed in a behavioral
specification. For the illustration of the formal definitions and concepts intro-
duced hereafter, we will focus here only on the locomotion aspect of the robot's
legs. We assume a simple component architecture: The locomotion of each leg is
coordinated by a controller component, called LegC , and the leg motorization is
wrapped in another component, named Leg .

2 Modal I/O-Transition Systems with Data Constraints

Modal I/O-transition systems (MIOs) have been introduced in [9,11] as a formal-
ism to describe the behavior of reactive, concurrent components which interact
via matching input and output actions. MIOs distinguish between “may” and
“must” transitions where the former specify which transitions are allowed in a
refinement while the latter specify which transitions are mandatory (i.e. must
be preserved) in any refinement. Formally, a MIO S is given by a tuple S =
( states S , start S ,act S ,Δ may
S

,Δ must
S

)ofasetofstates states S , the initial state

act in S being the dis-
joint union of sets of input, output and internal actions respectively, a may-
transition relation Δ may
S

states S ,asetofactions act S = act i S act out

S

start S ∈

⊆ states S × act S × states S , and a must-transition

Δ ma S . To deal with data constraints, we want to be able to
specify pre- and postconditions for the actions on modal transitions. Hence, we
must use more involved labels than simple action names.

relation Δ must
S

⊆

Operations. Instead of actions, we consider operations which may have formal pa-
rameters. An operation op is of the form opname ( Par )where Par is a (possibly
empty) set of formal parameters. We write par ( op ) to refer to the formal param-
eters of an operation op .An I/O-operation signature O prov O req O int O =