Software & Systems Modeling

, Volume 18, Issue 2, pp 837–863 | Cite as

A method for testing and validating executable statechart models

  • Tom MensEmail author
  • Alexandre Decan
  • Nikolaos I. Spanoudakis
Theme Section Paper


Statecharts constitute an executable language for modelling event-based reactive systems. The essential complexity of statechart models solicits the need for advanced model testing and validation techniques. In this article, we propose a method aimed at enhancing statechart design with a range of techniques that have proven their usefulness to increase the quality and reliability of source code. The method is accompanied by a process that flexibly accommodates testing and validation techniques such as test-driven development, behaviour-driven development, design by contract, and property statecharts that check for violations of behavioural properties during statechart execution. The method is supported by the Sismic tool, an open-source statechart interpreter library in Python, which supports all the aforementioned techniques. Based on this tooling, we carry out a controlled user study to evaluate the feasibility, usefulness and adequacy of the proposed techniques for statechart testing and validation.


Statechart Executable modeling Behaviour-driven development Design by contract Runtime verification 



We express our gratitude to Jordi Cabot, Simon Van Mierlo, Gauvain Devillez and Mathieu Goeminne, and several anonymous reviewers for providing comments on earlier versions of this article.


  1. 1.
    Aravantinos, V., Voss, S., Teufl, S., Hölzl, F., Schätz, B.: AutoFOCUS 3: tooling concepts for seamless, model-based development of embedded systems. In: International Workshop on Model-Based Architecting of Cyber-Physical and Embedded Systems and International Workshop on UML Consistency Rules, Volume 1508 of CEUR Workshop Proceedings, pp. 19–26. (2015)Google Scholar
  2. 2.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Beck, K.: Test-Driven Development by Example. Addison-Wesley, Reading (2002)Google Scholar
  4. 4.
    Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: International Conference Computer Aided Verification (CAV), pp. 363–367. Springer (2001)Google Scholar
  5. 5.
    Bunse, C., Klingert, S., Schulze, T.: Greenslas: supporting energy-efficiency through contracts. In: International Workshop on Energy Efficient Data Centers, pp. 54–68. Springer (2012)Google Scholar
  6. 6.
    Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)CrossRefGoogle Scholar
  7. 7.
    Cariou, E., Ballagny, C., Feugas, A., Barbier, F.: Contracts for model execution verification. In: European Conference Modelling Foundations and Applications (ECMFA), Volume 6698 of Lecturer Notes in Computer Science, pp. 3–18. Springer (2011)Google Scholar
  8. 8.
    Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)CrossRefGoogle Scholar
  9. 9.
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: A language framework for expressing checkable properties of dynamic software. In: International SPIN Model Checking and Software Verification Workshop, Volume 1885 of Lecturer Notes in Computer Science, pp. 205–223. Springer (2000)Google Scholar
  10. 10.
    Cossentino, M., Gaglio, S., Garro, A., Seidita, V.: Method fragments for agent design methodologies: from standardisation to research. Int. J. Agent Oriented Softw. Eng. 1(1), 91–121 (2007)CrossRefGoogle Scholar
  11. 11.
    Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: International Conference on Financial Cryptography and Data Security, pp. 79–94. Springer (2016)Google Scholar
  12. 12.
    Dietrich, I., Dressler, F., Dulz, W., German, R.: Validating UML simulation models with model-level unit tests. In: International Conference Simulation Tools and Techniques (SIMUTools) (2010)Google Scholar
  13. 13.
    Douglas, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, Reading (1999)Google Scholar
  14. 14.
    Drusinsky, D.: Semantics and runtime monitoring of TLCharts: statechart automata with temporal logic conditioned transitions. In: Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), Electronic Notes in Theoretical Computer Science, Volume 113, pp. 3–21 (2005)Google Scholar
  15. 15.
    Drusinsky, D.: Modeling and Verification Using UML Statecharts. Elsevier Science, Amsterdam (2006)Google Scholar
  16. 16.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering, pp. 411–420. ACM (1999)Google Scholar
  17. 17.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Esmaeilsabzali, S., Day, N.A., Atlee, J.M., Niu, J.: Deconstructing the semantics of big-step modelling languages. Requir. Eng. 15(2), 235–265 (2010)CrossRefGoogle Scholar
  19. 19.
    Estler, H., Furia, C.A., Nordio, M., Piccioni, M., Meyer, B.: Contracts in practice. In: International Symposium on Formal Methods (FM), Volume 8442 of Lecturer Notes in Computer Science, pp. 230–246. Springer (2014)Google Scholar
  20. 20.
    Fabbri, S.C.P.F., Maldonado, J.C., Sugeta, T., Masiero, P.C.: Mutation testing applied to validate specifications based on statecharts. In: International Symposium on Software Reliability Engineering (ISSRE), pp. 210–219. IEEE Computer Society (1999)Google Scholar
  21. 21.
    Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141–175 (2013)Google Scholar
  22. 22.
    Gnesi, S., Latella, D., Massink M.: Model checking UML statechart diagrams using JACK. In: International Symposium on High-Assurance Systems Engineering (HASE), pp. 46–55. IEEE Computer Society (1999)Google Scholar
  23. 23.
    Gogolla, M., Hamann, L., Hilken, F., Sedlmeier, M.: Modeling behavior with interaction diagrams in a UML and OCL tool. In: Behavior Modeling—Foundations and Applications, BM-FA 2009–2014, Revised Selected Papers, Volume 6368 of Lecturer Notes in Computer Science, pp. 31–58. Springer (2015)Google Scholar
  24. 24.
    Gogolla, M., Büttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Gomaa, H.: Designing Software Product Lines with UML: From Use Cases to Pattern-Based Software Architectures. Addison Wesley, Reading (2004)Google Scholar
  26. 26.
    Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: International Conference on Model Driven Engineering Languages and Systems, Volume 7590 of Lecturer Notes in Computer Science, pp. 235–251. Springer (2012)Google Scholar
  27. 27.
    Harel, D.: On visual formalisms. Commun. ACM 31(5), 514–530 (1988)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Comput. 30(7), 31–42 (1997)CrossRefGoogle Scholar
  29. 29.
    Harel, D., Kugler, H.: The Rhapsody Semantics of Statecharts (or, on the Executable Core of the UML), Volume LNCS 3147. Springer, Berlin (2004)Google Scholar
  30. 30.
    Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996)CrossRefGoogle Scholar
  31. 31.
    Henderson-Sellers, B., Ralyté, J.: Situational method engineering: state-of-the-art review. J. Univers. Comput. Sci. 16(3), 424–478 (2010)Google Scholar
  32. 32.
    Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: International Symposium on Rules and Rule Markup Languages for the Semantic Web, pp. 167–183. Springer (2016)Google Scholar
  33. 33.
    Lazar, I., Motogna, S., Parv, B.: Behaviour-driven development of foundational UML components. Electron. Notes Theor. Comput. Sci. 264(1), 91–105 (2010). (Int’l Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA))CrossRefGoogle Scholar
  34. 34.
    Leavens, G.T., Cheon, Y.: Design by Contract with JML. Technical report, Iowa State University (2006)Google Scholar
  35. 35.
    Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Program. 78(5), 293–303 (2009). (The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07))CrossRefzbMATHGoogle Scholar
  36. 36.
    Magee, J.: Behavioral analysis of software architectures using LTSA. In: International Conference on Software Engineering, pp. 634–637. ACM (1999)Google Scholar
  37. 37.
    Meyer, B.: Contract-driven development. In: International Conference on Fundamental Approaches to Software Engineering (FASE), Volume 4422 of Lecturer Notes in Computer Science, p. 11. Springer (2007)Google Scholar
  38. 38.
    Meyer, B.: Applying "design by contract". IEEE Comput. 25(10), 40–51 (1992)CrossRefGoogle Scholar
  39. 39.
    North, D.: Behavior modification: the evolution of behavior-driven development. Better Software (2006)Google Scholar
  40. 40.
    Object Management Group. Object Constraint Language, Version 2.4. OMG Document Number: formal/2014-02-03. URL: (2014)
  41. 41.
    Object Management Group. OMG Unified Modeling Language (OMG UML), Version 2.5. OMG Document Number: formal/2015-03-01. URL: (2015)
  42. 42.
    OMG. Software and Systems Process Engineering Meta-Model Specification. Version 2.0. Technical Report OMG Document Number: Formal/2008-04-01. Object Management Group (2008)Google Scholar
  43. 43.
    Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Soft. Eng. 40(5), 427–449 (2014)CrossRefGoogle Scholar
  44. 44.
    Samek, M.: Practical UML Statecharts in C/C++: Event-Driven Programming for Embedded Systems, 2nd edn. CRC Press, Boca Raton (2008)CrossRefGoogle Scholar
  45. 45.
    Sen, K.: Concolic testing. In: International Conference on Automated Software Engineering, pp. 571–572. ACM (2007)Google Scholar
  46. 46.
    Spanoudakis, N., Moraitis, P.: The agent modeling language (AMOLA). In: Dochev, D., Pistore, M., Traverso, P. (eds.) Artificial Intelligence: Methodology, Systems, and Applications, Volume 5253 of Lecture Notes in Computer Science, pp. 32–44. Springer, Berlin (2008)Google Scholar
  47. 47.
    Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Van Mierlo, S., Ergin, H.: AToMPM: a web-based modeling environment. In: Joint Proceedings of MODELS’13 Invited Talks, Demonstration Session, Poster Session, and ACM Student Research Competition, Volume 1115, CEUR Workshop Proceedings (2013)Google Scholar
  48. 48.
    Topalidou-Kyniazopoulou, A., Spanoudakis, N.I., Lagoudakis, M.G.: A CASE tool for robot behavior development. In: Chen, X., Stone, P., Sucar, L.E., Zant, T. (eds.) RoboCup 2012: Robot Soccer World Cup XVI. Lecture Notes in Computer Science, vol. 7500, pp. 225–236. Springer, Berlin (2013)CrossRefGoogle Scholar
  49. 49.
    Trakhtenbrot, M.: New mutations for evaluation of specification and implementation levels of adequacy in testing of statecharts models. In: Testing: Academic and Industrial Conference Practice and Research Techniques (MUTATION), pp. 151–160 (2007)Google Scholar
  50. 50.
    Wynne, M., Hellesoy, A.: The Cucumber Book: Behaviour-Driven Development for Testers and Developers. Pragmatic Bookshelf. ISBN: 978-1-93435-680-7. (2012)

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Software Engineering Lab, Faculty of SciencesUniversity of MonsMonsBelgium
  2. 2.Applied Mathematics and Computers Laboratory, School of Production Engineering and ManagementTechnical University of CreteChaniaGreece

Personalised recommendations