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.
M. Farrell–This work is funded by a Government of Ireland Postgraduate Grant from the Irish Research Council.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)
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)
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)
Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978)
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
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)
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
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
Mosses, P.D. (ed.): Casl Reference Manual. The Complete Documentation of the Common Algebraic Specification Language. LNCS, vol. 2960. Springer, Heidelberg (2004)
O’Reilly, L.: Structured Specification with Processes and Data. Ph.D. thesis, Swansea University, Swansea, U.K (2012)
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)
Roggenbach, M.: CSP-CASL - a new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42–71 (2006)
Sanella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Springer, Heidelberg (2012)
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
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)
Schneider, S., Treharne, H., Wehrheim, H.: The behavioural semantics of Event-B refinement. Formal Aspects Comput. 26, 251–280 (2014)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Farrell, M., Monahan, R., Power, J.F. (2017). Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability. In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-68690-5_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68689-9
Online ISBN: 978-3-319-68690-5
eBook Packages: Computer ScienceComputer Science (R0)