Interface automata Conference Paper


Author(s): de Alfaro, Luca; Henzinger, Thomas A
Title: Interface automata
Affiliation
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 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.
Conference Title: FSE: Foundations of Software Engineering
Conference Dates: September 10-14, 2001
Conference Location: Vienna, Austria
Publisher: ACM  
Location: New York, NY, USA
Date Published: 2001-06-01
Start Page: 109
End Page: 120
DOI: 10.1145/503209.503226
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work