Subject: Formal semantics | [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] | Theorem proving | B to HLL translation validation | Model animation | Autre
International audience; To check the correctness of heterogeneous models of a complex critical system is challenging to meet the certification standard. Such guarantee can be provided by embedding the heterogeneous models into an integrated modelling framework. This wor... View more
 N. Benaissa, D. Bonvoisin, A. Feliachi, and J. Ordioni, “The perf approach for formal verification,” in RSSRail, 2016, pp. 203-214.
 J. Ordioni, N. Breton, and J.-L. Colaço, “HLL v.2.7 Modelling Language Specification,” RATP, Tech. Rep., 2018. [Online]. Available: https://hal.archives-ouvertes.fr/hal-01799749
 N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The synchronous data flow programming language lustre,” Proceedings of the IEEE, vol. 79, no. 9, pp. 1305-1320, 1991.
 J. R. Abrial, The B-book: assigning programs to meanings. Cambridge Univ. Press, 1996.
 M. R. Prasad, A. Biere, and A. Gupta, “A survey of recent advances in sat-based formal verification,” International Journal on Software Tools for Technology Transfer, vol. 7, no. 2, pp. 156-173, 2005.
 A. Feliachi, D. Bonvoisin, C. Samira, and J. Ordioni, “Formal verification of system-level safety properties on railway software,” 2016.
 “Ieee standard for communications-based train control (cbtc) performance and functional requirements,” IEEE Std 1474.1-1999, 1999.
 A. Halchin, A. Feliachi, N. K. Singh, Y. A. Ameur, and J. Ordioni, “Bperfect - applying the PERF approach to B based system developments,” in RSSRail, 2017, pp. 160-172.
 ClearSy, “Atelier b user manual version 4.0,” 2009.
 M. J. C. Gordon, R. Milner, and C. P. Wadsworth, Edinburgh LCF, ser. Lecture Notes in Computer Science. Springer, 1979, vol. 78. [Online]. Available: https://doi.org/10.1007/3-540-09724-4