Modal Interface Automata
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1136/pdf |
| _version_ | 1797268678921682944 |
|---|---|
| author | Gerald Lüttgen Walter Vogler |
| author_facet | Gerald Lüttgen Walter Vogler |
| author_sort | Gerald Lüttgen |
| collection | DOAJ |
| description | 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\v{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. |
| first_indexed | 2024-04-25T01:36:18Z |
| format | Article |
| id | doaj.art-1e05ad8cba95494e96a9c0872c0b229a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:18Z |
| publishDate | 2013-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-1e05ad8cba95494e96a9c0872c0b229a2024-03-08T09:29:28ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-08-01Volume 9, Issue 310.2168/LMCS-9(3:4)20131136Modal Interface AutomataGerald LüttgenWalter VoglerDe 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\v{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.https://lmcs.episciences.org/1136/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theorycomputer science - software engineering |
| spellingShingle | Gerald Lüttgen Walter Vogler Modal Interface Automata Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory computer science - software engineering |
| title | Modal Interface Automata |
| title_full | Modal Interface Automata |
| title_fullStr | Modal Interface Automata |
| title_full_unstemmed | Modal Interface Automata |
| title_short | Modal Interface Automata |
| title_sort | modal interface automata |
| topic | computer science - logic in computer science computer science - formal languages and automata theory computer science - software engineering |
| url | https://lmcs.episciences.org/1136/pdf |
| work_keys_str_mv | AT geraldluttgen modalinterfaceautomata AT waltervogler modalinterfaceautomata |