Abstract
While refinement gives a formal underpinning to the development of dependable control systems, such models are difficult to communicate and reason about in a non-formal sense, particularly for validation by non-specialist industrial partners. Here we present a visualisation of, and guidance for, event B refinement using a specialisation of UML statemachines. Furthermore, we introduce design patterns and process rules that are aimed at assisting in the software development process leading to correct refinements. The specialisation will be incorporated into the UML-B notation to be integrated with the Event B platform developed by the RODIN project.
Work done within the EU research project RODIN: IST 511599.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R., Mussat, L.: Event B Reference Manual (2001), http://www.atelierb.societe.com/ressources/evt2b/eventb_reference_manual.pdf
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.R., Cansell, D., Méry, D.: Refinement and Reachability in Event B. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 222–241. Springer, Heidelberg (2005)
Abrial, J.R., Hallerstede, S., Mehta, F., Métayer, C., Voisin, L.: Specification of Basic Tools and Platform. RODIN Deliverable D10 [17] (2005)
Back, R.J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131–142 (1983)
Back, R.J.R., Sere, K.: From modular systems to action systems. Software - Concepts and Tools 17, 26–39 (1996)
Back, R.J.R., von Wright, J.: Refinement calculus: A systematic introduction. Springer, New York (1998)
Boström, P., Jansson, M., Waldén, M.: A healthcare case study: Fillwell. TUCS Technical Reports No 569, Turku Centre for Computer Science, Finland
Booch, G., Jacobson, I., Rumbaugh, J.: The Unified Modeling Language - a Reference Manual. Addison-Wesley, Reading (1998)
Butler, M., Waldén: Distributed system development in B. In: Proceedings of the 1st Conference on the B Method, Nantes, France, November 1996, pp. 155–168 (1996)
ClearSy. Atelier B. http://www.atelierb.societe.com/
Idani, A., Ledru, Y.: Dynamic Graphical UML Views from Formal B Specifications. Information and Software Technology 48(3), 154–169 (2006)
Katz, S.M.: A superimposition control construct for distributed systems. ACM Transactions on Programming Languages and Systems 15(2), 337–356 (1993)
Métayer, C., Abrial, J.R., Voisin, L.: Event-B Language, RODIN Deliverable D7 [17] (2005)
UML 2.0 Superstructure Specification, Document-formal/05-07-04 (UML Superstructure Specification, v2.0) (August 2005), (accessed 16.07.2006), http://www.omg.org/cgi-bin/doc?formal/05-07-04
Petre, L., Troubitsyna, E., Waldén, M., Boström, P., Engblom, N., Jansson, M.: Methodology of integration of formal methods within the healthcare case study. TUCS Technical Reports No 436, Turku Centre for Computer Science, Finland (October 2001)
Rigorous Open Development Environment for Complex Systems (RODIN) - IST 511599, http://rodin.cs.ncl.ac.uk/
Sekerinski, E.: Graphical Design of Reactive Systems. In: Proceedings of the 2nd International B Conference, Montpellier, France, April 1998, pp. 182–197. Springer, Heidelberg (1998)
Simons, A.: A theory of regression testing for behaviourally compatible object types. Software Testing, Verification and Reliability 16(3), 133–156; (UKTest 2005 Special Edition)
Snook, C., Butler, M.: U2B Downloads, http://www.ecs.soton.ac.uk/~cfs/U2Bdownloads.htm
Snook, C., Butler, M.: U2B -a tool for translating UML-B models into B. In: Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design, Springer, Heidelberg (2004)
Snook, C., Oliver, I., Butler, M.: The UML-B profile for formal systems modelling in UML. In: Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design, Springer, Heidelberg (2004)
Snook, C., Tsiopoulos, L., Waldén, M.: A case study in requirement analysis of control systems using UML and B. In: Proceedings of RCS 2003 - International workshop on Refinement of Critical Systems: Methods, Tools and Experience, Turku, Finland (June 2003), http://www.esil.univ-mrs.fr/~spc/rcs03/rcs03.html
Snook, C., Waldén, M.: Refinement of Statemachines using Hierarchical States, Choice Points and Joins. In: Proceedings of the EPSRC RefineNet Workshop, UK (2005)
Troubitsyna, E.: Stepwise Development of Dependable Systems. Turku Centre for Computer Science, TUCS, Ph.D. thesis No.29 (June 2000)
Waldén, M., Sere, K.: Reasoning About Action Systems Using the B-Method. Formal Methods in Systems Design 13(5-35) (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Snook, C., Waldén, M. (2006). Refinement of Statemachines Using Event B Semantics. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_15
Download citation
DOI: https://doi.org/10.1007/11955757_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)