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

systems concerns the compatibility of interacting components: whenever an in-
terface specification allows that a message may be issued, then the communica-
tion partner should be in a (control) state where it must be able to accept the
message [4].
In this paper we extend MIOs by taking into account the specification of data
constraints which enhance transitions with pre- and postconditions describing
the admissible data states of a component before and after the execution of
an operation. We distinguish, like in MIOs, between input, output and inter-
nal messages and, additionally, between provided, required and internal state
variables. Provided and internal state variables are local to a component and de-
scribe the data states a component can adopt. In contrast to the internal state
variables, provided state variables are visible to the user of a component. Re-
quired state variables belong also to the interface specification of a component,
however, they are not related to the data states of the component itself but to
the data states the component can observe in its environment. On this basis we
study (synchronous) composition, refinement and compatibility of modal I/O-
transition systems with data constraints (MIODs). In addition to relationships
between control states, we take special care of the relationships between data
constraints in all these cases. For instance, considering compatibility, the condi-
tion concerning control flow compatibility is extended to take into account data
states: the caller of an operation must ensure that the precondition of the opera-
tion provided by the callee is satisfied and, conversely, the callee must guarantee
that after the execution of the operation the postcondition expected by the caller
holds. Thus, the compatibility notion takes into account the mutual assumptions
and guarantees of communicating components guided by the idea that specifi-
cations provide contracts which must match when components are composed.
Our main result shows that our framework satisfies the basic requirements of
an interface theory: refinement is compositional and compatibility is preserved
by refinement. Thus modal I/O-transition systems with data constraints sup-
port reusability and independent implementability of components via interface
specifications.
Related Work. Specifications of control flow and of changing data states are often
considered separately from each other. While transition systems are a popular
formalism to specify the temporal ordering of messages, invariants and pre- and
postconditions are commonly used to specify the effects of operations w.r.t. data
states. Though approaches like CSP-OZ [8] offer means to specify both aspects,
they still lack a fully integrated treatment since their expressive power is limited
to cases where the effect of an operation on data states must be independent of
the control-flow behavior of a component. Other related approaches are based on
symbolic transition systems (STS) [7,1] but STS are mainly focussing on model
checking and not on interface theories supporting the (top down) development
of concurrent systems by refinement. Most closely related to our work is the
study of Mouelhi et al. [12] who consider an extension of the theory of interface
automata [6] to data states. Their approach does, however, not take into account
modalities of transitions and modal refinements. There is also no discrimination