Systematic Verification and Testing

  • Dana Dghaym
  • Tomas Fischer
  • Thai Son Hoang
  • Klaus Reichl
  • Colin Snook
  • Rupert SchlickEmail author
  • Peter Tummeltshammer


In this chapter, we present a process pattern for model based specification, verification and testing. It combines concepts of behaviour driven development (BDD), graphical and formal, mathematical modelling, formal verification techniques, acceptance testing and model based testing. The rigorous approach helps to ensure that for highly dependable systems, dependability (e.g. safety) requirements are fulfilled and both the specified and the implemented behaviour are as desired. It helps bridging the gap between natural language or semi-formal requirements and mathematical abstraction. Furthermore, it addresses the issue that formal modelling expertise and domain knowledge are rarely held by the same set of people.


  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. Transfer 12(6), 447–466 (2010)CrossRefGoogle Scholar
  3. 3.
    Back, R., Sere, K.: Stepwise refinement of action systems. In: International Conference on Mathematics of Program Construction, pp. 115–138. Springer, Berlin (1989)Google Scholar
  4. 4.
    Buschmann, F., Henney, K., Schmidt, D.C.: Pattern-Oriented Software Architecture, 4th edn. Wiley Series in Software Design Patterns, Wiley (2007). Google Scholar
  5. 5.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Fellner, A., Krenn, W., Schlick, R., Tarrach, T., Weissenbacher, G.: Model-based, mutation-driven test case generation via heuristic-guided branching search. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 56–66. ACM, New York (2017)Google Scholar
  7. 7.
    Herzner, W., Sieverding, S., Kacimi, O., Böde, E., Bauer, T., Nielsen, B.: Expressing best practices in (risk) analysis and testing of safety-critical systems using patterns. In: 25th IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops, Naples, Italy, November 3–6, 2014, pp. 299–304. IEEE, Piscataway (2014)Google Scholar
  8. 8.
    Hoang, T.S.: An introduction to the Event-B modelling method. In: Industrial Deployment of System Engineering Methods, pp. 211–236. Springer, Berlin (2013)Google Scholar
  9. 9.
    Hoang, T.S., Dghaym, D., Snook, C.F., Butler, M.J.: A composition mechanism for refinement-based methods. In: 22nd International Conference on Engineering of Complex Computer Systems, ICECCS 2017, pp. 100–109. IEEE, Piscataway (2017)Google Scholar
  10. 10.
    Krenn, W., Schlick, R., Aichernig, B.K.: Mapping UML to labeled transition systems for test-case generation. In: Formal Methods for Components and Objects, pp. 186–207. Springer, Berlin (2010)CrossRefGoogle Scholar
  11. 11.
    Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)CrossRefGoogle Scholar
  12. 12.
    North, D.: Introducing BDD. Better Software Magazine (2006)Google Scholar
  13. 13.
    Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2015)CrossRefGoogle Scholar
  14. 14.
    Smart, J.F.: BDD in Action: Behavior-Driven Development for the Whole Software Life cycle. Manning Publications Company, Shelter Island (2014)Google Scholar
  15. 15.
    Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, pp. 29–30. Toulouse, France (2014).
  16. 16.
    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
  17. 17.
    Wynne, M., Hellesøy, A.: The Cucumber Book: Behaviour-Driven Development for Testers and Developers. Pragmatic Programmers, LLC, Raleigh (2012)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Dana Dghaym
    • 1
  • Tomas Fischer
    • 2
  • Thai Son Hoang
    • 1
  • Klaus Reichl
    • 2
  • Colin Snook
    • 1
  • Rupert Schlick
    • 3
    Email author
  • Peter Tummeltshammer
    • 2
  1. 1.ECSUniversity of SouthamptonSouthamptonUK
  2. 2.Thales Austria GmbHViennaAustria
  3. 3.AIT Austrian Institute of Technology GmbHViennaAustria

Personalised recommendations