Part of the book series:Communications in Computer and Information Science ((CCIS,volume 929))
Included in the following conference series:
640Accesses
Abstract
Mathematical techniques known as formal methods have demonstrated great value in building safe-by-design systems and processes. However, the booming industry automation and digitalization require sustained advances in engineering approaches to address the emerging control-command challenges, all with respect to the highest quality and safety standards. Our research suggests that combining different formal techniques can contribute in enriching the specification and verification phases of industrial systems design. In this paper, we show - and illustrate through an ERTMS (European Rail Traffic Management System) L3 case study addressing the calculation of Movement Authority - how the mapping of two specific features of Petri Nets (PNs) and Event-B, namely Lists and sequences, could fit in the model transformation of PNs to B-machines and be used both in modeling and verification.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Boudi, Z., Ben-Ayed, R., Collart-Dutilleul, S., Nolasco, T., Haloua, M.: A CPN/B method transformation framework for railway safety rules formal validation. Eur. Transp. Res. Rev.9(2), 13 (2017)
Boudi, Z., Collart-Dutilleul, S., et al.: Colored Petri nets formal transformation to B machines for safety critical software development. In: 2015 International Conference on Industrial Engineering and Systems Management (IESM), pp. 12–18. IEEE (2015)
Combemale, B., Crégut, X., Garoche, P.L., Thirioux, X.: Essay on semantics definition in MDE. An instrumented approach for model verification. J. Softw. (JSW)4(9), 943–958 (2009)
Istoan, P.: Methodology for the derivation of product behaviour in a software product line. Ph.D. thesis, Université Rennes 1 (2013)
Bon, P., Dutilleul, S.C.: From a solution model to a B model for verification of safety properties. J. UCS19(1), 2–24 (2013)
Sun, P., Bon, P., Collart-Dutilleul, S.: A joint development of coloured petri nets and the b method in critical systems. J. Univ. Comput. Sci.21(12), 1654–1683 (2015)
Korečko, Š., Sobota, B.: Petri Nets to B-language transformation in software development. Acta Polytech. Hung.11(6), 187–206 (2014)
Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1. Springer, Heidelberg (2013)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer9(3–4), 213–254 (2007)
Ratzer, A.V., et al.: CPN tools for editing, simulating, and analysing coloured Petri Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 450–462. Springer, Heidelberg (2003).https://doi.org/10.1007/3-540-44919-1_28
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Eurasian Economic Union Group: Hybrid ERTMS/ETCS Level 3: Principles, Brussels, Belgium (July 2017)
Author information
Authors and Affiliations
Ecole Mohammadia d’Ingénieurs, Med V University, Rabat, Morocco
Zakaryae Boudi & Mohamed Haloua
Institut de Recherche Technologique Railenium, 59300, Famars, France
Abderrahim Ait Wakrime
IFSTTAR-Lille, 20 Rue Elisée Reclus, BP 70317, 59666, Villeneuve d’Ascq Cedex, France
Simon Collart-Dutilleul
- Zakaryae Boudi
You can also search for this author inPubMed Google Scholar
- Abderrahim Ait Wakrime
You can also search for this author inPubMed Google Scholar
- Simon Collart-Dutilleul
You can also search for this author inPubMed Google Scholar
- Mohamed Haloua
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toAbderrahim Ait Wakrime.
Editor information
Editors and Affiliations
Cadi Ayyad University, Marrakesh, Morocco
El Hassan Abdelwahed
ISAE-ENSMA, Chasseneuil-du-Poitou, France
Ladjel Bellatreche
LIRIS Lab, University Lyon 1, IUT, Villeurbanne Cedex, France
Djamal Benslimane
Computer Science and Information Technology, University of Bologna, Cesena, Italy
Matteo Golfarelli
ISAE-ENSMA, Chasseneuil-du-Poitou, France
Stéphane Jean
LORIA, Nancy, France
Dominique Mery
University of Hyogo, Himeji, Japan
Kazumi Nakamatsu
University of Houston, Houston, TX, USA
Carlos Ordonez
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Boudi, Z., Ait Wakrime, A., Collart-Dutilleul, S., Haloua, M. (2018). Petri Nets to Event-B: Handling Mathematical Sequences Through an ERTMS L3 Case. In: Abdelwahed, E.,et al. New Trends in Model and Data Engineering. MEDI 2018. Communications in Computer and Information Science, vol 929. Springer, Cham. https://doi.org/10.1007/978-3-030-02852-7_5
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-030-02851-0
Online ISBN:978-3-030-02852-7
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative