L. de Alfaro and T.A. Henzinger.
Interface Automata.
In
ESEC/FSE 01: Proceedings of the Joint 8th European Software
Engineering Conference and 9th ACM SIGSOFT International
Symposium on the Foundations of Software Engineering,
pages 109-120, ACM Press, 2001.
Abstract
Postscript
PDF
Abstract
Conventional type systems specify interfaces in terms of values and domains.
We present a light-weight formalism that captures the
temporal
aspects of software component interfaces.
Specifically, we use an automata-based language to capture both input
assumptions about the order in which the methods of a component are called,
and output guarantees about the order in which the component calls
external methods.
The formalism supports automatic compatibility checks between interface
models, and thus constitutes a type system for component interaction.
Unlike traditional uses of automata, our formalism is based on an
optimistic approach to composition, and on an
alternating
approach to design refinement.
According to the optimistic approach, two components are compatible if there
is
some environment that can make them work together.
According to the alternating approach, one interface refines another if it
has weaker input assumptions, and stronger output guarantees.
We show that these notions have game-theoretic foundations that lead to
efficient algorithms for checking compatibility and refinement.