Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10610))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

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

References

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

    Book  MATH  Google Scholar 

  2. 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)

    Article  Google Scholar 

  3. 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)

    Google Scholar 

  4. 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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  9. 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

    Google Scholar 

  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)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

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

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Book  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Maynooth University, Maynooth, Ireland

    Marie Farrell, Rosemary Monahan & James F. Power

Authors
  1. Marie Farrell
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rosemary Monahan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. James F. Power
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marie Farrell .

Editor information

Editors and Affiliations

  1. Xidian University, Xi’an, China

    Zhenhua Duan

  2. University of Oxford, Oxford, United Kingdom

    Luke Ong

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation