Modal interface automata

DOI10.2168/LMCS-9(3:4)2013MaRDI QIDQ5891133zbMATH OpenOpenAlexFDO

Authors Gerald Lüttgen, Walter Vogler

Publication date 6 September 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.3050

zbMATH Keywords

conjunctiondisjunctiondisjunctive modal transition systemsinterface automatainterface theoriesmodal interface automatamodal transition systems

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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 Benev{s} 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.

Recommendations

• Modal Interface Automata
• ACTL for modal interface automata
• Modal scenarios as automata
• Modal I/O Automata for Interface and Product Line Theories
• Automated Technology for Verification and Analysis
• Nondeterministic modal interfaces
• Nondeterministic modal interfaces
• An algebraic theory of interface automata

Cited in

(24)

• Generalized interface automata with multicast synchronization
• A linear-time branching-time perspective on interface automata
• Moving from interface theories to assembly theories
• Refinement checking on parametric modal transition systems
• Richer interface automata with optimistic and pessimistic compatibility
• ACTL for modal interface automata
• A generalised theory of interface automata, component compatibility and error
• Error-pruning in interface automata
• Nondeterministic modal interfaces
• Interface automata for shared memory
• A generalised theory of interface automata, component compatibility and error
• A modal interface theory for component-based design
• On weak modal compatibility, refinement, and the MIO workbench
• Combining partial specifications using alternating interface automata
• Nondeterministic modal interfaces
• Modal specification theories for component-based design
• Interface automata with complex actions: limiting interleaving in interface automata
• Interface theories for concurrency and data
• Automated Technology for Verification and Analysis
• Modal I/O Automata for Interface and Product Line Theories
• Modal Interface Automata
• From interface automata to hypercontracts
• Interface automata for shared memory
• Hypercontracts

This page was built for publication: Modal interface automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5891133)