Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2018: Formal Methods and Software Engineering pp 21–36Cite as

Behaviour-Driven Formal Model Development

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11232))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Google Scholar 

  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)

    Article  Google Scholar 

  3. 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

    Chapter  Google Scholar 

  4. Dghyam, D., Hoang, T.S., Snook, C.: Requirements document, scenarios, and models for lift examples, May 2018. https://doi.org/10.5258/SOTON/D0604

  5. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  Google Scholar 

  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 (2017)

    Google Scholar 

  7. 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

    Chapter  Google Scholar 

  8. 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

    Chapter  MATH  Google Scholar 

  9. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  11. Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transf. (STTT) 10(2), 185–203 (2008)

    Article  Google Scholar 

  12. Ladenberger, L.: BMotion studio for ProB project website, January 2016. http://stups.hhu.de/ProB/w/BMotion_Studio

  13. 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

    Article  Google Scholar 

  14. 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

    Google Scholar 

  15. Smart, J.F.: BDD in Action: Behavior-Driven Development for the Whole Software Life cycle. Manning Publications Company, Shelter Island (2014)

    Google Scholar 

  16. 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

    Article  MathSciNet  Google Scholar 

  17. 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

    Google Scholar 

  18. Wynne, M., Hellesøy, A.: The Cucumber Book: Behaviour-Driven Development for Testers and Developers. Pragmatic Programmers LLC, Raleigh (2012)

    Google Scholar 

Download references

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

  1. ECS, University of Southampton, Southampton, UK

    Colin Snook, Thai Son Hoang, Dana Dghyam & Michael Butler

  2. Thales Austria GmbH, Vienna, Austria

    Tomas Fischer

  3. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Rupert Schlick

  4. Southwest Jiaotong University, Chengdu, China

    Keming Wang

Authors
  1. Colin Snook
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thai Son Hoang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dana Dghyam
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Butler
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Tomas Fischer
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Rupert Schlick
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Keming Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Colin Snook .

Editor information

Editors and Affiliations

  1. University of Auckland, Auckland, New Zealand

    Jing Sun

  2. Peking University, Beijing, China

    Meng Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation