nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability

verfasst von : Marie Farrell, Rosemary Monahan, James F. Power

Erschienen in: Formal Methods and Software Engineering

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In this paper we present a formal framework designed to facilitate interoperability between the Event-B specification language and the process algebra CSP. Our previous work used the theory of institutions to provide a mathematically sound framework for Event-B, and this enables interoperability with CSP, which has already been incorporated into the institutional framework. This paper outlines a comorphism relationship between the institutions for Event-B and CSP, leveraging existing tool-chains to facilitate verification. We compare our work to the combined formalism Event-B\(\Vert \)CSP and use a supporting example to illustrate the benefits of our approach.

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

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

Vorheriges Kapitel Verifying Temporal Properties of C Programs via Lazy Abstraction

Nächstes Kapitel Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems

http://www.cs.nuim.ie/~mfarrell/extended.pdf.

Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH

Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef

Farrell, M., Monahan, R., Power, J.F.: Providing a semantics and modularisation constructs for Event-B using institutions. In: International Workshop on Algebraic Development Techniques (2016)

Fitzgerald, J., Larsen, P.G., Woodcock, J.: Foundations for model-based engineering of systems of systems. In: Aiguier, M., Boulanger, F., Krob, D., Marchal, C. (eds.) Complex Systems Design & Management, pp. 1–19. Springer, Cham (2014)

Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)MathSciNetCrossRefMATH

Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978)CrossRef

Iliasov, A.: On Event-B and control flow. Technical report, Newcastle University, Newcastle Upon Tyne, U.K (2009)

Isobe, Y., Roggenbach, M.: CSP-Prover - a proof tool for the verification of scalable concurrent systems. Inf. Media Technol. 5(1), 32–39 (2010)

Knapp, A., Mossakowski, T., Roggenbach, M., Glauer, M.: An institution for simple UML state machines. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 3–18. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_1

10.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef

11.

Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_40 CrossRef

12.

Mossakowski, T., Roggenbach, M.: Structured CSP – a process algebra as an institution. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 92–110. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71998-4_6 CrossRef

13.

Mosses, P.D. (ed.): Casl Reference Manual. The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004)MATH

14.

O’Reilly, L.: Structured Specification with Processes and Data. Ph.D. thesis, Swansea University, Swansea, U.K (2012)

15.

O’Reilly, L., Roggenbach, M., Isobe, Y.: CSP-CASL-Prover: a generic tool for process and data refinement. Electron. Notes Theor. Comput. Sci. 250(2), 69–84 (2009)CrossRefMATH

16.

Roggenbach, M.: CSP-CASL - a new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42–71 (2006)MathSciNetCrossRefMATH

17.

Sanella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Springer, Heidelberg (2012)CrossRef

18.

Schneider, S., Treharne, H., Wehrheim, H.: A CSP approach to control in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 260–274. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16265-7_19 CrossRef

19.

Schneider, S., Treharne, H., Wehrheim, H.: Bounded retransmission in Event-B\(\Vert \)CSP: a case study. Electron. Notes Theor. Comput. Sci. 280, 69–80 (2011)CrossRef

20.

Schneider, S., Treharne, H., Wehrheim, H.: The behavioural semantics of Event-B refinement. Formal Aspects Comput. 26, 251–280 (2014)MathSciNetCrossRefMATH

21.

Snook, C., Butler, M.: UML-B and Event-B: an integration of languages and tools. In: IASTED International Conference on Software Engineering, pp. 336–341, Innsbruck, Austria (2008)

Titel: Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability
verfasst von: Marie Farrell
Rosemary Monahan
James F. Power
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-68690-5_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner