A CPN/B method transformation framework for railway safety rules formal validation

European Transport Research Review - Tập 9 Số 2 - 2017
Zakaryae Boudi1, Rahma Ben-Ayed2, El Miloudi El Koursi2, Simon Collart-Dutilleul2, Thomas Nolasco3, Mohamed Haloua1
1Ecole Mohammadia d'Ingénieurs
2Évaluation des Systèmes de Transports Automatisés et de leur Sécurité
3ClearSy Systems Engineering

Tóm tắt

Từ khóa


Tài liệu tham khảo

Ghazel M (2014) Formalizing a subset of ERTMS/ETCS specifications for verification purposes. Transportation research-Part C: Emerging technologies 42: 60-75. DOI: 10.1016/j.trc.2014.02.002 , ELSEVIER, http://www.sciencedirect.com/science/journal/0968090X, 0968-090X

Jabri S, El-Koursi EM, Bourdeauhuy TH, Lemaire E (2010) European railway traffic management system validation using UML/Petri nets modelling strategy. Eur Transp Res Rev (ETRR), ECTRI 2:113-128. DOI: 10.1007/s12544-010-0030-5 , Springer, http://www.springer.com/engineering/mechanical+eng/journal/12544

Boudi Z, El-Koursi EM, Collart-Dutilleul S, Khaddour M (2014) High level Petri net modeling for railway safety critical scenarios. In: Proc. of 10th FORMS/FORMAT symposium on formal methods. Braunchweig, pp 65-75

Ben Ayed R, Collart-Dutilleul S, Bon P, Idani A, Ledru Y (2014) B formal validation of ERTMS/ETCS railway operating rules. In: Ait Ameur Y, Schewe K-D (eds) ABZ 2014, LNCS, vol 8477. Springer, Heidelberg, pp 124–129

Sun P, Collart-dutilleul S, Bon P (2014) Formal modeling methodology of French railway interlocking system via HCPN. 14th International conference on Railway Engineering Design and Optimization, Rome, Italy

Antoni M (2009) Formal validation method for computerized railway interlocking systems. Computers Industrial Engineering. CIE 2009. International Conference on, pp 1532–1541

Murata T (1989) Petri nets: properties, analysis and applications, an invited survery paper. Proc IEEE 77(4):541–580

Genrich HJ (1991) Predicate/Transition Nets. K. Jensen and G. Rozenberg (Eds.): High-level Petri Nets. Theory and Application. Springer-Verlag, pp 3-43

Reisig W (1991) Petri nets and algebraic specifications. Theor Comput Sci 80(1):1–34

Jensen K (1992) Coloured Petri Nets – Basic Concepts, Analysis Methods and Practical Use-Vol. 1. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, pp 1-X, 1–236

Jensen K, Kristensen LM, Wells L (2007) Coloured Petri nets and CPN tools for Modelling and validation of concurrent systems. Int J Softw Tools Technol Trans (STTT) 9(3–4):213–254

Ratzer AV, Wells L, Lassen HM, Laursen M, Qvortrup JF, Stissing MS, Westergaard M, Christensen S, Jensen K (2003) CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets. Proc. of 24th International Conference on Applications and Theory of Petri Nets (Petri Nets 2003). Lecture notes in computer Science, vol 2679. Springer-Verlag Berlin, pp 450–462

Lalouette J, Brinzei N, Malasse O, Caron R, Scherb F, Aubry J-F (2010) Modeling and performance assessment of a railway signaling system integrating ETCS and BAL using colored Petri nets. Version 1, Sixth International French Conference of Automatic, CIFA 2010, Nancy, France

Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press

Stuckenschmidt H (2002) Ontology-Based Information Sharing in Weakly Structured Environments. PhD thesis, University of Vrije

Redjimi M, Boukelkoul S (2013) Algorithmic tools for the transformation of Petri nets to DEVS. Informatica 37:411–418

Aubrecht P, Zakova M, Kouba Z (2005) Ontology Transformation Using Generalized Formalism. Znalosti, roèníku conference, pp. 154-161, V©B-TUO

Combemale B, Crégut X, Garoche PL, Thirioux X (2009) Essay on semantic definitions in MDE - an instrumented approach for model verification. JSW, vol 4(9):943–958

Istoan P. Methodology for the derivation of product behavior in a Software Product Line. PhD thesis, University of Rennes 1, University of Luxembourg, February 2013

Bon P, Collart-Dutilleul S (2013) From a solution model to a B model for verification of safety properties. J UCS 19(1):2–24

Korečko S, Sobota B (2014) Petri nets to B-language transformation in software development. Acta Plotechnica Hungarica 11(6):2014

UNISIG. Subset-039: FIS for the RBC/RBC Handover. April 2009

Bon P, Collart-Dutilleul S, Sun P. Study of implementation of ERTMS with respect to French national rules using a B centred methodology, International Conference on Industrial Engineering and Systems Management IESM’2013 October 28–October 30 Rabat – Morocco