Interfaces: A game-theoretic framework for reasoning about component-based systems

Abstract

Traditional type systems specify interfaces in terms of values and domains. When we apply a function to an argument, or when we compose two functions, we have to check that their types match. Interface models extend type systems with the ability to reason about the dynamic behavior of design components. For instance, interface models are able to capture temporal-ordering constraints on component interaction, such as constraints on the ordering of method calls or protocol messages, timing constraints on a component's input and output signals, and constraints on the usage of shared resources. Like type systems, interfaces specify both the input assumptions a component makes on its environment and the output guarantees it provides. Interfaces are based on two-player games in which the system plays against the environment. The moves of the environment (player Input) represent the inputs that the system can receive from the environment, that is, the input assumption of the system. Symmetrically, the moves of the system (player Output) represent the possible outputs that can be generated by the system. Interfaces are built around the concepts of (1) well-formedness, requiring that the input assumptions of an interface be satisfiable; (2) compatibility, asking whether two components can be used in a way that satisfies the input assumptions of both components; (3) composition of compatible interfaces; and (4) refinement, asking whether one component (being an implementation) correctly implements another one (being the specification). This paper provides a tutorial-style introduction to interfaces and discusses the basic concepts and ideas. In particular, we elaborate on the automaton-based interfaces from [12]and the timed interfaces from [14]. Due space limitations, we do not treat the notion of interface refinement, but we refer the reader to [12] and [10]. © 2004 Elsevier B.V. All rights reserved.