Interfaces: A Game-Theoretic Framework for Reasoning About Component-Based Systems

AbstractTraditional 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 [L. de Alfaro and T.A. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109–120. ACM Press, 2001] and the timed interfaces from [L. de Alfaro, T.A. Henzinger, and M.I.A. Stoelinga. Timed interfaces. In Proceedings of the Second International Workshop on Embedded Software (EMSOFT 2002), volume 2491 of Lect. Notes in Comp. Sci., pages 108–122. Springer-Verlag, 2002]. Due space limitations, we do not treat the notion of interface refinement, but we refer the reader to [L. de Alfaro and T.A. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109–120. ACM Press, 2001] and [L. de Alfaro. Game models for open systems. In Int. Symposium on Verification celebrating Zohar Manna's 64th Birthday, volume 2772 of Lect. Notes in Comp. Sci. Springer-Verlag, 2003]