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 compatability 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.
['Luca de Alfaro', 'Thomas A. Henzinger']
Interface automata