W.: Richer interface automata with optimistic and pessimistic compatibility. ECEASST 66 (2013), an extended version has been submitted to Acta Informatica

Abstract: Modal transition systems are a popular semantic underpinning of inter-face theories, such as Nyman et al.’s IOMTS and Bauer et al.’s MIO, which facili-tate component-based reasoning of concurrent systems. Our interface theory MIA repaired a compositional flaw of IOMTS-refinement and introduced a conjunction operator. In this paper, we first modify MIA to properly deal with internal com-putations including internal must-transitions, which were largely ignored already in IOMTS. We then study a MIA variant that adopts MIO’s pessimistic – rather than IOMTS ’ optimistic – view on component compatibility and define, for the first-time in a pessimistic, non-deterministic setting, conjunction and disjunction on interfaces. For the pessimistic MIA variant we also provide a mechanism for extending alphabets when refining interfaces, which is a desired feature in practice. We illustrate our advancements via a small example