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

A Modal Interface Theory with Data Constraints

Sebastian S. Bauer 1 , Rolf Hennicker 1 , and Michel Bidoit 2

1 Ludwig-Maximilians-Universitat Munchen, Germany
2 Laboratoire Specification et Verification,
CNRS & ENS de Cachan, France

Abstract. For the design of component-based software, the behavioral
specification of component interfaces is crucial. We propose an exten-
sion of the theory of modal I/O-transition systems by Larsen et al. to
cope with both control flow and data states of reactive components at the
same time. In our framework, transitions model incoming or outgoing op-
eration calls which are constrained by pre- and postconditions expressing
the mutual assumptions and guarantees of the receiver and the sender
of a message. We define a new interface theory by adapting synchronous
composition, modal refinement and modal compatibility to the case of
modal I/O-transition systems with data constraints. We show that in this
formalism modal compatibility is preserved by refinement and modal re-
finement is preserved by composition which are basic requirements for
any interface theory.

1 Introduction

A rigorous discipline of component-based software development relies strongly on
interface specifications which describe the observable behavior of components [6].
Thereby, behavior is often understood from a control-flow oriented perspective
considering the sequences of actions a component can perform when interacting
with its environment. Of equal importance is, however, the aspect of changing
data - owned by a component - when certain actions of the component are
performed. We claim that the integrated treatment of control flow and data
change in the context of concurrent, reactive components is not yet suciently
understood and therefore needs further investigation.
Building on previous work on the semantics of behavior protocols for com-
ponents with data states [3] we propose an interface theory on the basis of
modal I/O-transition systems (MIOs) introduced in [9]. A particular advantage
of modal transition systems is that they distinguish between “may” and “must”
transitions which leads to a powerful refinement notion [11]: the may-transitions
determine which actions are permitted in a refinement while the must-transitions
specify which actions must be present in a refinement and hence in any imple-
mentation. In this way it is possible to provide abstract, loose specifications in
terms of may-transitions and to fix in a stepwise way the must-transitions until
an implementation, represented by a MIO with must-transitions only, is reached.
Another aspect which can be conveniently formalized with modal I/O-transition