Interface Automata

Interface Automata
by Luca de Alfaro, Thomas A. Henzinger

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.

The idea of expressing order of message exchange as type is certainly not new (as anyone exposed to web service choreography hype can tell - oh, just kidding, of course the theory is much older). However, the specific approach looks interesting (not the least because of appealing to game semantics).

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Some comments

  1. The way the optimistic approach to composability relates to the pessimistic one reminds me the relationship between principal typings and principal types
  2. As composition of interfaces is associative, there might be a nice categorical reformulation of the theory
  3. The limitation mentioned after Example 3.7 was a real surprise to me - I expected the approach inspired by game theory would handle "must/may" more carefully.

A little help...

I find this very interesting, but am having a tough time with the notation of Illegal(P,Q) in page 8. Could anyone help enlighten me?

Which part are you having

Which part are you having trouble with? A brief overview of Figure 3 is that you take the product of P-states and Q-states, such that whenever a state is shared between the two you check that it is not in the mutually exclusive sets. So if some a is shared between the automata then it cannot be an output of one automata without being an input of the other (because it could lead to deadlock in one automata if the environment is malicious). The conjunctions are tighter binding than the disjunction floating in the middle (which is quite an odd looking layout), and the bracketing is for the dot which I'm reading as 'such that', same as the bar.

Specifically, I was having a

Specifically, I was having a hard time with the layout of the disjunction and the dot. I wasn't sure if that notation was just kind of odd, or it actually meant something different than what you describe. Thanks for your help!