Advertisement

Shared Event Composition/Decomposition in Event-B

  • Renato Silva
  • Michael Butler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)

Abstract

The construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques supporting reuse and allowing formal combination of sub-components through refinement steps. Sub-components can result from a design or architectural goal and a refinement framework should allow them to be further developed, possibly in parallel. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronised shared events and shared states are not allowed. We define the necessary proof obligations to ensure valid compositions and decompositions. We also show that shared event composition preserves refinement proofs, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding sub-components. A case study applying these two techniques is illustrated using Rodin, the Event-B toolset.

Keywords

formal methods composition decomposition reuse Event-B design techniques specification 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Jackson, D.: Structuring Z specifications with views. ACM Trans. Softw. Eng. Methodol. 4(4), 365–389 (1995)CrossRefGoogle Scholar
  2. 2.
    Zave, P., Jackson, M.: Conjunction as Composition. ACM Trans. Softw. Eng. Methodol. 2(4), 379–411 (1993)CrossRefGoogle Scholar
  3. 3.
    Jones, C.B.: Wanted: a compositional approach to concurrency. In: Programming Methodology, pp. 5–15. Springer-Verlag New York, Inc, New York (2003)CrossRefGoogle Scholar
  4. 4.
    Poppleton, M.: The Composition of Event-B Models. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 209–222. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefzbMATHGoogle Scholar
  6. 6.
    Abrial, J.R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundam. Inf. 77(1-2), 1–28 (2007)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Butler, M.: An Approach to the Design of Distributed Systems with B AMN. In: Till, D., P. Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 221–241. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  8. 8.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International Series in Computer Science (1985)Google Scholar
  9. 9.
    Morgan, C.: Of wp and CSP. In: Beauty is our Business: a Birthday Salute to Edsger W. Dijkstra, pp. 319–326. Springer-Verlag New York, Inc., New York (1990)CrossRefGoogle Scholar
  10. 10.
    Back, R.-J.R., Kurki-Suonio, R.: Decentralization of Process Nets with Centralized Control. In: PODC 1983: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, pp. 131–142. ACM, New York (1983)CrossRefGoogle Scholar
  11. 11.
    Abrial, J.R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  12. 12.
    Rodin: RODIN project Homepage (September 2008), http://rodin.cs.ncl.ac.uk (accessed July 27, 2010)
  13. 13.
    Abrial, J.R., Butler, M.J., Hallerstede, S., Voisin, L.: An Open Extensible Tool Environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Spivey, J.M.: The Z Notation: a Reference Manual. Prentice-Hall, Inc., Englewood Cliffs (1989)zbMATHGoogle Scholar
  15. 15.
    Butler, M.J.: A CSP Approach to Action Systems. PhD thesis, Oxford University (1992)Google Scholar
  16. 16.
    Butler, M.: Stepwise Refinement of Communicating Systems. Science of Computer Programming 27(2), 139–173 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Butler, M.: Synchronisation-Based Decomposition for Event-B. In: RODIN Deliverable D19 Intermediate Report on Methodology, pp. 47–57 (2006)Google Scholar
  18. 18.
    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. International Journal on Software Tools for Technology Transfer, STTT (April 2010)Google Scholar
  19. 19.
    Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition Tool for Event-B. Software: Practice and Experience 41(2), 199–208 (2011)Google Scholar
  20. 20.
    Silva, R., Butler, M.: Parallel Composition Using Event-B (July 2009), http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B (accessed July 27, 2010)
  21. 21.
    Back, R.-J.R.: Refinement Calculus, part II: Parallel and Reactive Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67–93. Springer, Heidelberg (1990)Google Scholar
  22. 22.
    Abadi, M., Lamport, L.: Composing Specifications. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 1–41. Springer, Heidelberg (1990)Google Scholar
  23. 23.
    Woodcock, J., Dickinson, B.: Using VDM with Rely and Guarantee-Conditions. In: Bloomfield, R.E., Jones, R.B., Marshall, L.S. (eds.) VDM 1988. LNCS, vol. 328, pp. 434–458. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  24. 24.
    Bellegarde, F., Julliand, J., Kouchnarenko, O.: Synchronized Parallel Composition of Event Systems in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 436–457. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. 25.
    Butler, M., Waldén, M.: Distributed System Development in B. Technical Report TUCS-TR-53, Turku Centre for Computer Science, 14 (1996)Google Scholar
  26. 26.
    Hoang, T., Abrial, J.R.: Event-B Decomposition for Parallel Programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 319–333. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Renato Silva
    • 1
  • Michael Butler
    • 1
  1. 1.School of Electronics and Computer ScienceUniversity of SouthamptonUK

Personalised recommendations