, European Committee for Electrotechnical Standardization EN 50128: Railway applications -Communication, signalling and processing systems -Software for railway control and protection systems, CENELEC Tech. Rep, 2011.

J. Abrial, The B Book -Assigning Programs to Meanings, 1996.

M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte, VCC: Contract-based modular verification of concurrent C, 2009 31st International Conference on Software Engineering, Companion Volume, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5071046

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO, ser. LNCS, 2005.
DOI : 10.1007/11804192_17

F. Randimbivololona, J. Souyris, P. Baudin, A. Pacalet, J. Raguideau et al., Applying formal proof techniques to avionics software: a pragmatic approach, the Wold Congress on Formal Methods in the Development of Computing Systems (FM'99), pp.1798-1815, 1999.
DOI : 10.1007/3-540-48118-4_45

. Frama-c, Frama-C homepage

K. Hartig, J. Gerlach, J. Soto, and J. Busse, Formal Specification and Automated Verification of Safety-Critical Requirements of a Railway Vehicle with Frama-C/Jessie, pp.145-153, 2010.
DOI : 10.1007/978-3-642-14261-1_15

J. Burghardt, J. Gerlach, K. Hartig, H. Pohl, and K. Völlinger, Formal Specification and Automated Verification of Railway Software with Frama-C, Fraunhofer FOKUS, 2012.
URL : https://hal.archives-ouvertes.fr/cea-01835639

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language, v1, 2012.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Software Engineering and Formal Methods, SEFM, ser. LNCS, 2012.
DOI : 10.1007/978-3-642-33826-7_16

J. Burghardt, J. Gerlach, K. Hartig, H. Pohl, and J. S. Völlinger,

Y. Moy and C. Marché,

L. Correnson, Z. Dargaye, and . Plug, , 2012.

C. A. Hoare, An axiomatic basis for computer programming, pp.576-580, 1969.

. Alt-ergo, Alt-ergo homepage

C. Barrett and C. Tinelli, CVC3 homepage Simplify homepage

S. International, Yices homepage

J. Busse, Sicherheitsanforderungsspezifikation Diesellok Institut für Bahntechnik GmbH (IfB) Technical Note, 2007.

, Squish Coco Code Coverage Measurement for C/C++ or C#, 2012.

R. Sc-205, Formal Methods Supplement to DO-178C and DO- 278A (DO-333), Radio Technical Commission for Aeronautics (RTCA Inc.), Tech. Rep, 2011.