Top

Published in:

2019 | OriginalPaper | Chapter

A Generic Dynamic Logic with Applications to Interaction-Based Systems

Authors : Rolf Hennicker, Martin Wirsing

Published in: From Software Engineering to Formal Methods and Tools, and Back

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

We propose a generic dynamic logic with the usual diamond and box modalities over structured actions. Instead of using regular expressions of actions our logic is parameterised by the form of the actions which can be given by an arbitrary language for complex, structured actions. In particular, our logic can be instantiated by languages that describe complex interactions between system components. We study two instantiations of our logic for specifying global behaviours of interaction-based systems: one on the basis of global session types and the other one using UML sequence diagrams. Moreover, we show that our proposed generic logic, and hence all its instantiations, satisfy bisimulation invariance and a Hennessy-Milner theorem.

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 "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

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

previous chapter Logical Support for Bike-Sharing System Design

next chapter Ambiguity in Requirements Engineering: Towards a Unifying Framework

Städtische Galerie im Lenbachhaus, München, https://www.lenbachhaus.de/?L=1.

This means that for any atomic action a and any state s there are at most finitely many outgoing transitions labelled with a.

Andrade, L., et al.: AGILE: software architecture for mobility. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 1–33. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40020-2_1CrossRef

Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party sessions. Log. Methods Comput. Sci. 8(1), 1–45 (2012)MathSciNetCrossRef

Cengarle, M.V., Knapp, A., Mühlberger, H.: Interactions. In: Lano, K. (ed.) UML 2-Semantics and Applications, pp. 205–248. Wiley, Hoboken (2009)

Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_10CrossRef

Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing and Hölzl [22], pp. 390–407

Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)CrossRef

Object Management Group. Unified Modeling Language 2.5. http://www.omg.org/spec/UML/2.5. Accessed 21 May 2019

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)CrossRef

Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32, 137–162 (1985)MathSciNetCrossRef

10.

Hennicker, R.: Role-based development of dynamically evolving esembles. In: Fiadeiro, J.L., Ţuţu, I. (eds.) WADT 2018. LNCS, vol. 11563, pp. 3–24. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-23220-7_1CrossRef

11.

Hennicker, R., Wirsing, M.: Dynamic logic for ensembles. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 32–47. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03424-5_3CrossRef

12.

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), pp. 273–284. ACM (2008)

13.

Knapp, A., Mossakowski, T.: UML interactions meet state machines-an institutional approach. In: Bonchi, F., König, B. (eds.) 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, 12–16 June 2017, Ljubljana, Slovenia, LIPIcs, vol. 72, pp. 15:1–15:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

14.

Knapp, A., Wuttke, J.: Model checking of UML 2.0 interactions. In: Kühne, T. (ed.) MODELS 2006. LNCS, vol. 4364, pp. 42–51. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69489-2_6CrossRef

15.

Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL 2015, pp. 221–232 (2015)

16.

Micskei, Z., Waeselynck, H.: The many meanings of UML 2 sequence diagrams: a survey. Softw. Syst. Model. 10(4), 489–514 (2011)CrossRef

17.

Morin, R.: Recognizable sets of message sequence charts. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 523–534. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45841-7_43CrossRef

18.

Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. J. Appl. Log. 10(1), 2–31 (2012)MathSciNetCrossRef

19.

ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication requirements for team automata. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 256–277. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59746-1_14CrossRef

20.

ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312–328. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15545-6_20CrossRef

21.

Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Log. Algebr. Meth. Program. 95, 17–40 (2018)MathSciNetCrossRef

22.

Wirsing, M., Hölzl, M. (eds.): Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20401-2CrossRef

Title: A Generic Dynamic Logic with Applications to Interaction-Based Systems
Authors: Rolf Hennicker
Martin Wirsing
Publisher: Springer International Publishing
Book: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_11

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner