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.
Similar content being viewed by others
Notes
Flash is a registered trademark of Adobe Systems Inc.
References
Specification Case Studies in RAISE. Springer, London, UK (2002)
Abrial JR (1996) The B book. Cambridge University Press, Cambridge
Abrial JR (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge
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
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
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
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
Bjørner D (2006) Software engineering 3: domains, requirements, and software design (texts in theoretical computer science, an EATCS series). Springer, New York
Bjørner D (2007) Development of transportation systems. In: International symposium on leveraging applications of formal methods, Verification and Validation (ISOLA)
Bjørner D (2009) DOMAIN ENGINEERING: technology management, research and engineering. JAIST, Japan
Butler M (2002) A system-based approach to the formal development of embedded controllers for a railway. Des Autom Embed Syst 6:355–366
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
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
Clearsy (2009) User manual of Atelier B, version 4.0
Czarnecki K, Eisenecker UW (2000) Generative programming: methods, tools, and applications. ACM Press/Addison-Wesley Publishing Co., New York
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
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
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
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
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
TRL Group (1993) The RAISE specification language. Prentice-Hall Inc., Upper Saddle River
Hoare CAR (1985) Communicating sequential processes. Prentice Hall Int., Upper Saddle River
Jackson MA (1983) System development (Prentice-Hall International series in computer science). Prentice-Hall Inc., Upper Saddle River
Jones CB (1990) Systematic software development using VDM. 2nd edn. Prentice-Hall Inc., Upper Saddle River
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
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
van Lamsweerde A (2009) Requirements engineering: from system goals to UML models to software specifications. Wiley, Chichester
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
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
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
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/
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
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/
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
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
Milner R, Tofte M, Harper R, Macqueen D (1997) The definition of standard ML—revised. The MIT Press, Cambridge
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
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
Paulson LC (1996) ML for the working programmer. 2nd edn. Cambridge University Press, New York
Poppleton M (2008) The composition of Event-B models. In: 1st International conference on ASM, B and Z (ABZ2008). London, UK
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
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
Silva R, Pascal C, Hoang T, Butler M (2010) Decomposition tool for Event-B. In: Workshop on tool building in formal methods. Orford, Canada
Snook C, Butler M (2006) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15(1):92–122
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
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
Zave P, Jackson M (1997) Four dark corners for requirements engineering. ACM Trans Softw Eng Methodol 6(1):1–30
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
Corresponding author
Rights 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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00766-011-0120-5