Revisiting modal interface automata

Modern software systems are typically built of components that communicate through their external interfaces. A component´s behavior can be effectively described using finite state automata-based formalisms (e.g., statecharts [5]). The basic formalism, labelled transition systems, describes the behavior of a component in terms of states and labeled transitions. The more advanced formalisms, such as modal transition systems and interface automata, extend LTS to incorporate additional information related to interface operation controllability - distinguishing between input, output, and internal actions - and the possible partiality of a component´s specification - distinguishing between required and unknown (maybe) behaviors. Capturing the controllability and partiality aspects of a component´s specification facilitates (1) checking interface compatibility, (2) checking whether one component can safely replace another component, and (3) checking whether one specification is a proper refinement of another specification. In this paper, we study the existing definitions of these three types of checks, and then exemplify their limitations in the context of modal interface automata (MIA); MIA is a class of component behavior specifications that incorporates both controllability and partiality information. We outline a set of enhancements to MIA as possible solutions to the identified limitations.