Lüttgen, Gerald and Vogler, Walter - Modal Interface Automata

lmcs:1136 - Logical Methods in Computer Science, August 14, 2013, Volume 9, Issue 3
Modal Interface Automata

Authors: Lüttgen, Gerald and Vogler, Walter

De Alfaro and Henzinger's Interface Automata (IA) and Nyman et al.'s recent combination IOMTS of IA and Larsen's Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component shall satisfy multiple interfaces, while Larsen's MTS-conjunction is not closed and Beneš et al.'s conjunction on disjunctive MTS does not treat internal transitions. In addition, IOMTS-parallel composition exhibits a compositionality defect. This article defines conjunction (and also disjunction) on IA and disjunctive MTS and proves the operators to be 'correct', i.e., the greatest lower bounds (least upper bounds) wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS featuring explicit output-must-transitions while input-transitions are always allowed implicitly, is equipped with compositional parallel, conjunction and disjunction operators, and allows a simpler embedding of IA than Nyman's. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.'s modal interface theory does.


Source : oai:arXiv.org:1306.3050
DOI : 10.2168/LMCS-9(3:4)2013
Volume: Volume 9, Issue 3
Published on: August 14, 2013
Submitted on: November 5, 2012
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,Computer Science - Software Engineering


Share

Consultation statistics

This page has been seen 62 times.
This article's PDF has been downloaded 30 times.