Refinement of Statecharts with Run-to-Completion Semantics

  • Karla MorrisEmail author
  • Colin Snook
  • Thai Son Hoang
  • Robert Armstrong
  • Michael Butler
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1008)


Statechart modelling notations, with so-called ‘run to completion’ semantics and simulation tools for validation, are popular with engineers for designing systems. However, they do not support formal refinement and they lack formal static verification methods and tools. For example, properties concerning the synchronisation between different parts of a system may be difficult to verify for all scenarios, and impossible to verify at an abstract level before the full details of sub-states have been added. Open image in new window , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible, restricting instantiation and testing to a validation role. In this paper, we introduce a notion of refinement, similar to that of Open image in new window , into a ‘run to completion’ Statechart modelling notation, and leverage Open image in new window ’s tool support for proof. We describe the pitfalls in translating ‘run to completion’ models into Open image in new window refinements and suggest a solution. We illustrate the approach using our prototype translation tools and show by example, how a synchronisation property between parallel Statecharts can be automatically proven at an intermediate refinement level.


SCXML Statecharts Event-B iUML-B Refinement 



The authors would like to thank Jason Michnovicz for developing the IDS example used throughout the manuscript.


  1. 1.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  2. 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. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRefGoogle Scholar
  3. 3.
    David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002). Scholar
  4. 4.
    Eclipse Foundation: Sirius Project Website. Accessed Mar 2016
  5. 5.
    Eshuis, R.: Reconciling statechart semantics. Sci. Comput. Program. 74(3), 65–99 (2009)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Hansen, C., Syriani, E., Lucio, L.: Towards controlling refinements of statecharts. CoRR, abs/1503.07266 (2015)Google Scholar
  7. 7.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Hoang, T.S.: An introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211–236. Springer, Heidelberg (2013)Google Scholar
  9. 9.
    Hoang, T.S., Butler, M., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 251–261. Springer, Cham (2018). Scholar
  10. 10.
    Hoang, T.S., Snook, C., Ladenberger, L., Butler, M.: Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion studio, and co-simulation. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 360–375. Springer, Cham (2016). Scholar
  11. 11.
    Lima, L., et al.: An integrated semantics for reasoning about SysML design models using refinement. Softw. Syst. Model. 16(3), 875–902 (2017)CrossRefGoogle Scholar
  12. 12.
    Maraninchi, F.: The Argos language: graphical representation of automata and description of reactive systems. In: IEEE Workshop on Visual Languages (1991)Google Scholar
  13. 13.
    Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Cham (2016). Scholar
  14. 14.
    Meng, S., Naixiao, Z., Barbosa, L.S.: On semantics and refinement of UML statecharts: a coalgebraic view. In: Proceedings of the Second International Conference on Software Engineering and Formal Methods, SEFM 2004, pp. 164–173, September 2004Google Scholar
  15. 15.
    Miyazawa, A., Cavalcanti, A.: Formal refinement in SysML. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 155–170. Springer, Cham (2014). Scholar
  16. 16.
    Morris, K., Snook, C.: Reconciling SCXML statechart representations and Event-B lower level semantics. In: HCCV - Workshop on High-Consequence Control Verification (2016)Google Scholar
  17. 17.
    Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, Upper Saddle River (2004)Google Scholar
  18. 18.
    Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, Toulouse, France (2014).
  19. 19.
    Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)CrossRefGoogle Scholar
  20. 20.
    Snook, C., Savicks, V., Butler, M.: Verification of UML models by translation to UML-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 251–266. Springer, Heidelberg (2011). Scholar
  21. 21.
    Szasz, N., Vilanova, P.: Behavioral refinements of UML-Statecharts. Technical report RT 10–13, Universidad de la República, Montevideo, Uruguay (2010)Google Scholar
  22. 22.
    W3C: State chart XML SCXML: State machine notation for control abstraction. Accessed Sept 2015

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Karla Morris
    • 1
    Email author
  • Colin Snook
    • 2
  • Thai Son Hoang
    • 2
  • Robert Armstrong
    • 1
  • Michael Butler
    • 2
  1. 1.Sandia National LaboratoriesLivermoreUSA
  2. 2.University of SouthamptonSouthamptonUK

Personalised recommendations