Abstract
Formal systems modelling offers a rigorous system-level analysis resulting in a precise and reliable specification. However, some issues remain: Modellers need to understand the requirements in order to formulate the models, formal verification may focus on safety properties rather than temporal behaviour, domain experts need to validate the final models to ensure they fit the needs of stakeholders. In this paper we discuss how the principles of Behaviour-Driven Development (BDD) can be applied to formal systems modelling and validation. We propose a process where manually authored scenarios are used initially to support the requirements and help the modeller. The same scenarios are used to verify behavioural properties of the model. The model is then mutated to automatically generate scenarios that have a more complete coverage than the manual ones. These automatically generated scenarios are used to animate the model in a final acceptance stage. For this acceptance stage, it is important that a domain expert decides whether or not the behaviour is useful.
All data supporting this study are openly available from the University of Southampton repository at https://doi.org/10.5258/SOTON/D0604.
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
Similar content being viewed by others
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
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)
Back, R.J.R., Sere, K.: Stepwise refinement of action systems. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 115–138. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51305-1_7
Dghyam, D., Hoang, T.S., Snook, C.: Requirements document, scenarios, and models for lift examples, May 2018. https://doi.org/10.5258/SOTON/D0604
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)
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 (2017)
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). https://doi.org/10.1007/978-3-642-33170-1
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). https://doi.org/10.1007/978-3-319-91271-4_17
Krenn, W., Schlick, R., Aichernig, B.K.: Mapping UML to labeled transition systems for test-case generation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 186–207. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17071-3_10
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04570-7_17
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transf. (STTT) 10(2), 185–203 (2008)
Ladenberger, L.: BMotion studio for ProB project website, January 2016. http://stups.hhu.de/ProB/w/BMotion_Studio
Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2015). https://doi.org/10.1007/s10270-013-0391-z
Siqueira, F.L., de Sousa, T.C., Silva, P.S.M.: Using BDD and SBVR to refine business goals into an Event-B model: a research idea. In: 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 31–36, May 2017
Smart, J.F.: BDD in Action: Behavior-Driven Development for the Whole Software Life cycle. Manning Publications Company, Shelter Island (2014)
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006). https://doi.org/10.1145/1125808.1125811
Solis, C., Wang, X.: A study of the characteristics of behaviour driven development. In: 2011 37th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 383–387, August 2011
Wynne, M., Hellesøy, A.: The Cucumber Book: Behaviour-Driven Development for Testers and Developers. Pragmatic Programmers LLC, Raleigh (2012)
Acknowledgements
This work has been conducted within the ENABLE-S3 project that has received funding from the ECSEL Joint Undertaking under Grant Agreement no. 692455. This Joint Undertaking receives support from the European Unions HORIZON 2020 research and innovation programme and Austria, Denmark, Germany, Finland, Czech Republic, Italy, Spain, Portugal, Poland, Ireland, Belgium, France, Netherlands, United Kingdom, Slovakia, Norway.
ENABLE-S3 is funded by the Austrian Federal Ministry of Transport, Innovation and Technology (BMVIT) under the program “ICT of the Future” between May 2016 and April 2019. More information is at https://iktderzukunft.at/en/.
We also thank Thorsten Tarrach (Austrian Institute of Technology, Vienna, Austria) for his assistance with MoMuT.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Snook, C. et al. (2018). Behaviour-Driven Formal Model Development. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-02450-5_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02449-9
Online ISBN: 978-3-030-02450-5
eBook Packages: Computer ScienceComputer Science (R0)