Concurrent systems consist of multiple components; the design of such a system must: allow its specification to be composed from the component requirements; allow its implementation to be composed from the component capabilities; and support a process of step-wise refinement that demands more desired behaviors and prohibits more undesired ones. Such scenarios can be modeled by semantic frameworks that combine interface automata (IA), which describe the behavior of component-based systems, with modal transition systems (MTS), which describe with must-transitions and may-transitions which behavior every refinement of the system must respectively realize. However, this combination is problematic because unspecified inputs are forbidden in MTS while they lead to arbitrary behavior in IA.

This paper introduces the formalism of modal interface automata (MIA) that reconciles these views by introducing input-triggered may-transitions to a special state that can be refined in any way. The resulting theory of nondeterministic modal interfaces is elaborated in great detail by showing that it leads to a well-behaved parallel composition operator and to a quotient operator that constructs a component whose parallel composition with a given component refines a given specification, whose conjunction of specifications reflects multiple system perspectives, and whose refinement is compositional.

While the paper is mostly technical in nature, a final example demonstrates how MIA can be applied in practice. Furthermore, the authors have exploited MIA to enrich the programming language Go with behavioral types such that type checking implements refinement checking; the theory will also be implemented in formal methods tools.