Skip to main content
Log in

Utilizing Event-B for domain engineering: a critical analysis

  • Best Papers of RE'10: Requirements Engineering in a Multi-faceted World
  • Published:
Requirements Engineering Aims and scope Submit manuscript

Abstract

This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. Well-specified requirements are crucial for good software design; they depend on the understanding of the domain. Thus, domain engineering becomes an essential activity. The possibility to have a formal model of a domain, consistent with the use of formal methods for developing critical software working within it, is an important issue. Safety-critical domains, like transportation, exhibit interesting features, such as high levels of nondeterminism, complex interactions, stringent safety properties, and multifaceted timing attributes. The formal representation of these features is a challenging task. We explore the possibility of utilizing Event-B as a domain engineering tool. We discuss the problems we faced during this exercise and how we tackled them. Special attention is devoted to the issue of the validation of the model, in particular with a technique based on the animation of specifications. Event-B is mature enough to be an effective tool to model domains except in some areas, temporal properties mainly, where more work is still needed.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6

Similar content being viewed by others

Notes

  1. http://rodin-b-sharp.sourceforge.net.

  2. Flash is a registered trademark of Adobe Systems Inc.

  3. http://tacos.loria.fr.

  4. http://www.projet-cristal.org.

  5. http://www.animb.org.

References

  1. Specification Case Studies in RAISE. Springer, London, UK (2002)

  2. Abrial JR (1996) The B book. Cambridge University Press, Cambridge

    Book  MATH  Google Scholar 

  3. Abrial JR (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  4. Aziz B, Arenas AE, Bicarregui J, Ponsard C, Massonet P (2009) From goal-oriented requirements to Event-B specifications. In: First Nasa formal method symposium. California, US

  5. Baille G, Garnier P, Mathieu H, Roger PG (1999) Le cycab de l’INRIA rhônes-alpes. Technical Report RT-0229, INRIA—Rhônes-Alpes

  6. Bicarregui J, Arenas A, Aziz B, Massonet P, Ponsard C (2008) Towards modelling obligations in Event-B. In: Proceedings of the 1st international conference on Abstract State Machines, B and Z, ABZ ’08. Springer, New York, pp 181–194

  7. Bisztray D, Heckel R, Ehrig H (2008) Verification of architectural refactorings by rule extraction. In: FASE’08/ETAPS’08: proceedings of the Theory and practice of software, 11th international conference on Fundamental approaches to software engineering. Springer, Berlin, pp 347–361

  8. Bjørner D (2006) Software engineering 3: domains, requirements, and software design (texts in theoretical computer science, an EATCS series). Springer, New York

    Google Scholar 

  9. Bjørner D (2007) Development of transportation systems. In: International symposium on leveraging applications of formal methods, Verification and Validation (ISOLA)

  10. Bjørner D (2009) DOMAIN ENGINEERING: technology management, research and engineering. JAIST, Japan

    Google Scholar 

  11. Butler M (2002) A system-based approach to the formal development of embedded controllers for a railway. Des Autom Embed Syst 6:355–366

    Article  Google Scholar 

  12. Butler M (2009) Decomposition structures for Event-B. In: Proceedings of the 7th international conference on integrated formal methods, IFM ’09. Springer, Berlin, pp 20–38

  13. Cansell D, Mery D, Rehm J (2007) Time constraint patterns for event B development. In: Julliand J, Kouchnarenko O (eds) 7th International conference of B users, LNCS, vol 4355. Springer, New York, pp 140–154

  14. Clearsy (2009) User manual of Atelier B, version 4.0

  15. Czarnecki K, Eisenecker UW (2000) Generative programming: methods, tools, and applications. ACM Press/Addison-Wesley Publishing Co., New York

  16. Erasmy F, Sekerinski E (1995) Raise: a rigorous approach using stepwise refinement. In: Lewerentz C, Lindner T (eds) Formal development of reactive systems. Lecture Notes in Computer Science, vol 891. Springer, Berlin, pp 277–293

  17. Essamé D (2004) Handling safety critical requirements in system engineering using the b formal method. In: Heisel M, Liggesmeyer P, Wittmann S (eds) Computer safety, reliability, and security. Lecture Notes in Computer Science, vol 3219. Springer, Berlin, p 115

  18. Futatsugi K, Goguen JA, Jouannaud JP, Meseguer J (1985) Principles of obj2. In: POPL ’85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages. ACM, New York, pp 52–66

  19. Gondal A, Poppleton M, Snook C (2009) Feature composition—towards product lines of Event-B models. In: 1st International workshop on model-driven product line engineering. Twente, The Netherlands, pp 18–25

  20. Gørtz J (1994) Specifying safety and progress properties with rsl. In: Naftalin M, Denvir T, Bertran M (eds) FME ’94: industrial benefit of formal methods. Lecture Notes in Computer Science, vol 873. Springer, Berlin, pp 567–581

  21. TRL Group (1993) The RAISE specification language. Prentice-Hall Inc., Upper Saddle River

  22. Hoare CAR (1985) Communicating sequential processes. Prentice Hall Int., Upper Saddle River

  23. Jackson MA (1983) System development (Prentice-Hall International series in computer science). Prentice-Hall Inc., Upper Saddle River

    Google Scholar 

  24. Jones CB (1990) Systematic software development using VDM. 2nd edn. Prentice-Hall Inc., Upper Saddle River

    MATH  Google Scholar 

  25. Joochim T, Snook C, Poppleton M, Gravell A (2010) Timing diagrams requirements modeling using Event-B formal methods. In: IASTED international conference on software engineering (SE2010). Innsbruck, Austria

  26. Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143 (1977). http://doi.ieeecomputersociety.org/10.1109/TSE.1977.229904

    Google Scholar 

  27. van Lamsweerde A (2009) Requirements engineering: from system goals to UML models to software specifications. Wiley, Chichester

    Google Scholar 

  28. Lanoix A (2008) Event-B specification of a situated multi-agent system: study of a platoon of vehicles. In: 2nd IFIP/IEEE international symposium on theoretical aspects of software engineering (TASE). IEEE Computer Society, pp 297–304

  29. Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods, LNCS 2805. Springer, New York, pp 855–874

  30. Mashkoor A, Jacquot JP (2009) Incorporating animation in stepwise development of formal specification. Research report INRIA-00392996, LORIA, Nancy, France (2009). http://hal.inria.fr/inria-00392996/en

  31. Mashkoor A, Jacquot JP (2010) Transformational heuristics for animation—towards stepwise validation of specications. Research report HAL-00544261, LORIA, Nancy, France (2010). http://hal.archives-ouvertes.fr/hal-00544261/en/

  32. Mashkoor A, Jacquot JP, Souquières J (2009) Transformation Heuristics for formal requirements validation by animation. In: 2nd International workshop on the certification of safety-critical software controlled systems—SafeCert ’09. York, UK

  33. Mashkoor A, Jacquot JP, Souquières J (2009) B événementiel pour la modélisation du domaine: application au transport. In: Approches formelles dans l’Assistance au Développement de Logiciels (AFADL’2009), p 19. France Toulouse (2009). http://hal.inria.fr/inria-00326355/en/

  34. Mashkoor A, Matoussi A (2010) Towards validation of requirements models. In: 2nd International conference on abstract state machines (ASM), Alloy, B and Z (ABZ ’10). Orford, Canada

  35. Matoussi A, Gervais F, Laleau R (2008) A first attempt to express KAOS refinement patterns with event B. In: Proceedings of the International Conference on ASM, B and Z (ABZ). Lecture Notes in Computer Science. Springer, New York, pp 12–14

  36. Milner R, Tofte M, Harper R, Macqueen D (1997) The definition of standard ML—revised. The MIT Press, Cambridge

    Google Scholar 

  37. Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th International conference on automated deduction (CADE). Lecture Notes in Artificial Intelligence, vol 607. Springer, Saratoga, NY, pp 748–752

  38. Papatsaras A, Stoddart B (2002) Global and communicating state machine models in event driven b: a simple railway case study. In: ZB ’02: Proceedings of the 2nd international conference of B and Z users on formal specification and development in Z and B. Springer, London, pp 458–476

  39. Paulson LC (1996) ML for the working programmer. 2nd edn. Cambridge University Press, New York

    MATH  Google Scholar 

  40. Poppleton M (2008) The composition of Event-B models. In: 1st International conference on ASM, B and Z (ABZ2008). London, UK

  41. Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: Integrated formal methods-IFM 2010 integrated formal methods—8th international conference, IFM 2010, vol 6396. Springer, Berlin, pp 260–274

  42. Servat T (2006) BRAMA: a new graphic animation tool for B models. In: B 2007: Formal specification and development in B. Springer, New York, pp 274–276

  43. Silva R, Pascal C, Hoang T, Butler M (2010) Decomposition tool for Event-B. In: Workshop on tool building in formal methods. Orford, Canada

  44. Snook C, Butler M (2006) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15(1):92–122

    Article  Google Scholar 

  45. Yadav D, Butler M (2009) Verification of liveness properties in distributed systems. In: Second international conference on contemporary computing (IC3’09). Noida, India, pp 625–636

  46. Yang F, Jacquot JP (2011) Scaling up with Event-B: a case study. In: Havelund K (ed) Proceedings of the 3rd NASA formal methods symposium (NFM2011), p. to appear. LNCS

  47. Zave P, Jackson M (1997) Four dark corners for requirements engineering. ACM Trans Softw Eng Methodol 6(1):1–30

    Article  Google Scholar 

Download references

Acknowledgments

This work has been partially supported by ANR under project ANR-06-SETI-017 TACOS (http://tacos.loria.fr) and by Pôle de Compétitivité Alsace/Franche-Comté under CRISTAL project (http://www.projet-cristal.org).

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Atif Mashkoor.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Mashkoor, A., Jacquot, JP. Utilizing Event-B for domain engineering: a critical analysis. Requirements Eng 16, 191–207 (2011). https://doi.org/10.1007/s00766-011-0120-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00766-011-0120-5

Keywords

Navigation