Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 4/2019

17.04.2018 | Original Article

A generalised theory of Interface Automata, component compatibility and error

verfasst von: Sascha Fendrich, Gerald Lüttgen

Erschienen in: Acta Informatica | Ausgabe 4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Interface theories allow system designers to reason about the composability and compatibility of concurrent system components. Such theories often extend both de Alfaro and Henzinger’s Interface Automata and Larsen’s Modal Transition Systems, which leads, however, to several issues that are undesirable in practice: an unintuitive treatment of specified unwanted behaviour, a binary compatibility concept that does not scale to multi-component assemblies, and compatibility guarantees that are insufficient for software product lines. In this article we show that communication mismatches are central to all these problems and, thus, the ability to represent such errors semantically is an important feature of an interface theory. Accordingly, we present the error-aware interface theory EMIA, where the above shortcomings are remedied by introducing explicit fatal error states. In addition, we prove via a Galois insertion that EMIA is a conservative generalisation of the established Modal Interface Automata theory.
Nächster Artikel Equivalence checking of Petri net models of programs using static and dynamic cut-points

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Literatur
1.
Bauer, S.S., David, A., Hennicker, R., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Moving from specifications to contracts in component-based design. In: Fundamental Approaches to Software Engineering (FASE), Volume 7212 of LNCS, pp. 43–58. Springer, Berlin (2012)
2.
Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO Workbench. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6015 of LNCS, pp. 175–189. Springer, Berlin (2010)
3.
Beneš, N., Černa, I., Křetiínský, J.: Disjunctive modal transition systems and generalized LTL model checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University Brno (2010)
4.
Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A.: Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In: Concurrency Theory (CONCUR), Volume 8052 of LNCS, pp. 76–90. Springer, Berlin (2013)
5.
Beyer, D., Chakrabarti, A., Henzinger, T.A., Seshia, S.A.: An application of web-service interfaces. In: International Conference on Web Services (ICWS), pp. 831–838. IEEE (2007)
6.
Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. In: Theory and Practice of Computer Science (SOFSEM), Volume 8939 of LNCS, pp. 152–163. Springer, Berlin (2015)
7.
Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24–53 (2016)MathSciNetCrossRefMATH
8.
Bujtor, F., Vogler, W.: Error-pruning in interface automata. In: Theory and Practice of Computer Science (SOFSEM), Volume 8327 of LNCS, pp. 162–173. Springer, Berlin (2014)
9.
10.
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.Z.: A compositional specification theory for component behaviours. In: Programming Languages and Systems (ESOP), Volume 7211 of LNCS, pp. 148–168. Springer, Berlin (2012)
11.
Chilton, C.: An Algebraic Theory of Componentised Interaction. Ph.D. thesis, Oxford University (2013)
12.
Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Technical report RR-13-02, Oxford University (2013)
13.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)
14.
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE), pp. 109–120. ACM (2001)
15.
de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-Intensive Systems, Volume 195 of NATO Science, pp. 83–104. Springer, Berlin (2005)
16.
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT-Press, Cambridge (1989)CrossRef
17.
Emmi, M., Giannakopoulou, D., Păsăreanu, C.S.: Assume-guarantee verification for interface automata. In: Formal Methods (FM), Volume 5014 of LNCS, pp. 116–131. Springer, Berlin (2008)
18.
Fendrich, S.: Modal Interface Theories for Specifying Component-based Systems. Ph.D. thesis, Bamberg University (2017)
19.
Fendrich, S., Lüttgen, G.: A generalised theory of interface automata, component compatibility and error. In: Integrated Formal Methods (iFM), Volume 9681 of LNCS, pp. 160–175. Springer, Berlin (2016)
20.
Gareis, J.: Prototypical Integration of the Modal Interface Automata Theory in Google Go. Master’s thesis, Bamberg University (2015)
21.
Goessler, G., Raclet, J.-B.: Modal contracts for component-based design. In: Software Engineering and Formal Methods (SEFM), pp. 295–303. IEEE (2009)
22.
23.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)MATH
24.
Křetínský, J., Sickert, S.: MoTraS: a tool for modal transition systems and their extensions. In: Automated Technology for Verification and Analysis (ATVA), Volume 8172 of LNCS, pp. 487–491. Springer, Berlin (2013)
25.
Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, Volume 407 of LNCS, pp. 232–246. Springer, Berlin (1989)
26.
Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: Programming Languages and Systems (ESOP), Volume 4421 of LNCS, pp. 64–79. Springer, Berlin (2007)
27.
Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 1019 of LNCS, pp. 17–40. Springer, Berlin (1995)
28.
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Logic in Computer Scienc (LICS), pp. 108–117. IEEE (1990)
29.
Lohstroh, M., Lee, E.A.: An interface theory for the Internet of Things. In: Software Engineering and Formal Methods (SEFM), Volume 9276 of LNCS, pp. 20–34. Springer, Berlin (2015)
30.
Lüttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inform. 52(4–5), 305–336 (2015)MathSciNetCrossRefMATH
31.
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH
32.
Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1–2), 119–149 (2011)MathSciNetMATH
Metadaten
Titel
A generalised theory of Interface Automata, component compatibility and error
verfasst von
Sascha Fendrich
Gerald Lüttgen
Publikationsdatum
17.04.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 4/2019
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-018-0319-8

Premium Partner

    Bildnachweise