Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 4-5/2015

01-06-2015 | Original Article

Richer interface automata with optimistic and pessimistic compatibility

Authors: Gerald Lüttgen, Walter Vogler, Sascha Fendrich

Published in: Acta Informatica | Issue 4-5/2015

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Modal transition systems are a popular semantic underpinning of interface theories, such as Nyman et al.’s IOMTS and Bauer et al.’s MIO, which facilitate component-based reasoning for 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 computations 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 both the optimistic and pessimistic MIA variant, we also discuss mechanisms for extending alphabets when refining interfaces, which is a desired feature for perspective-based specification. We illustrate our advancements via a small example.
previous article Special issue on “Combining Compositionality and Concurrency”: part 2
next article Compositional verification of asynchronous concurrent systems using CADP

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Appendix
Available only for authorised users
Literature
1.
Bauer, S.: Modal Specification Theories for Component-based Design. Ph.D. Thesis, Faculty of Mathematics, Informatics and Statistics, LMU Munich, Germany (2012)
2.
Bauer, S., David, A., Hennicker, R., Larsen, K., Legay, A., Nyman, U., Wasowski, A.: Moving from specifications to contracts in component-based design. In: FASE, LNCS, vol. 7212, pp. 43–58. Springer, Berlin (2012)
3.
Bauer, S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO Workbench. In: TACAS, LNCS, vol. 6015, pp. 175–189. Springer, Berlin (2010)
4.
Beneš, N., Cerná, I., Křetínský, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.A. (eds.) ATVA, LNCS, vol. 6996, pp. 228–242. Springer, Berlin (2011)
5.
Beyer, D., Chakrabarti, A., Henzinger, T., Seshia, S.: An application of web-service interfaces. In: ICWS, pp. 831–838. IEEE (2007)
6.
Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. In: Software Seminar (SOFSEM) (2015)
7.
Bujtor, F., Vogler, W.: Failure semantics for modal transition systems. In: Application of Concurrency to Systems Design (ACSD) (2014)
8.
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.: A compositional specification theory for component behaviours. In: ESOP, LNCS, vol. 7211, pp. 148–168. Springer, Berlin (2012)
9.
Chilton, C.: An Algebraic Theory of Componentised Interaction. Ph.D. Thesis, Department of Computer Science, University of Oxford, UK (2013)
10.
de Alfaro, L., Henzinger, T.: Interface-based design. In: Engineering Theories of Software-Intensive Systems, NATO Science Series, vol. 195. Springer, Berlin (2005)
11.
Fahrenberg, U., Jan Křetínský, A.L., Traonouez, L.M.: Compositionality for quantitative specifications. In: Formal Aspects of Component Software, LNCS. Springer, Berlin (2014)
12.
Fischbein, D., Uchitel, S.: On correct and complete strong merging of partial behaviour models. In: Foundations of Software Engineering (SIGSOFT FSE), pp. 297–307 (2008)
13.
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)CrossRef
14.
Larsen, K.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, LNCS, vol. 407, pp. 232–246. Springer, Berlin (1990)
15.
Larsen, K., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: ESOP, LNCS, vol. 4421, pp. 64–79. Springer, Berlin (2007)
16.
Lüttgen, G., Vogler, W.: Modal interface automata. Log. Methods Comput. Sci. 9(3:4) (2013)
17.
Meyer, B.: Applying design by contract. IEEE Comput. 25(10), 40–51 (1992)CrossRef
18.
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)MATH
19.
Raclet, J., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 107, 1–32 (2011)MathSciNet
20.
Raclet, J.B.: Residual for component specifications. ENTCS 215, 93–110 (2008)
21.
Schäfer, M., Vogler, W.: Component refinement and CSC-solving for STG decomposition. Theor. Comput. Sci. 388(1–3), 243–266 (2007)MATHCrossRef
Metadata
Title
Richer interface automata with optimistic and pessimistic compatibility
Authors
Gerald Lüttgen
Walter Vogler
Sascha Fendrich
Publication date
01-06-2015
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 4-5/2015
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-014-0211-0

Other articles of this Issue 4-5/2015

Acta Informatica 4-5/2015 Go to the issue

Original Article

Denotational fixed-point semantics for constructive scheduling of synchronous concurrency

Editorial

Special issue on “Combining Compositionality and Concurrency”: part 2

Original Article

Compositional construction of most general controllers

Obituary

A life dedicated to informatics: an obituary for Prof. Friedrich L. Bauer

Original Article

Compositional verification of asynchronous concurrent systems using CADP

Premium Partner

    Image Credits