Abstract
An independent safety assessment of railway software systems is performed by RATP (Régie Autonome des Transports Parisiens) for all safety-critical systems before their deployment in its network. Whenever possible, this activity is performed using the PERF approach (Proof Executed over a Retro-engineered Formal model). PERF is a methodology which handles formal verification of already developed software. This approach is applied to a variety of software systems, developed using languages such as SCADE, Ada or C. It provides an alternative verification that can be applied for the independent safety assessment of critical systems used by RATP. In this paper, we propose the B-PERFect method to generalize the application of the PERF approach for critical systems which are based on the B method. In particular, this paper focuses on transformation strategy from B language to the pivot language of PERF: HLL. HLL is a synchronous data-flow language equipped with formal verification techniques. The differences between B and HLL are pointed out and the translation process is presented in this regard.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). doi:10.1007/3-540-48119-2_22
Benaissa, N., Bonvoisin, D., Feliachi, A., Ordioni, J.: The PERF approach for formal verification. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 203–214. Springer, Cham (2016). doi:10.1007/978-3-319-33951-1_15
Bert, D., Boulmé, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94–113. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45236-2_7
Bonichon, R., Déharbe, D., Lecomte, T., Medeiros, V.: LLVM-based code generation for B. In: Braga, C., Martí-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 1–16. Springer, Cham (2015). doi:10.1007/978-3-319-15075-8_1
Cataño, N., Wahls, T., Rueda, C., Rivera, V., Yu, D.: Translating B machines to JML specifications. In: SAC 2012, pp. 1271–1277. ACM (2012)
ClearSy: Atelier B user manual version 4.0 (2009)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
Espresso: Polychrony tool. http://www.irisa.fr/espresso/Polychrony
Fürst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323–338. Springer, Cham (2014). doi:10.1007/978-3-319-10181-1_20
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305–1320 (1991)
Kalla, H., Talpin, J.P., Berner, D., Besnard, L.: Automated translation of C/C++ models into a synchronous formalism. In: ECBS 2006. pp. 9–436, March 2006
Mammar, A., Laleau, R.: From a B formal specification to an executable code: application to the relational database domain. Info. Soft. Technol. 48(4), 253–279 (2006)
Méry, D., Singh, N.K.: Automatic code generation from EVENT-B models. In: SoICT 2011, pp. 179–188. ACM (2011)
Ge, N., Dieumegard, A., Jenn, E., Voisin, L.: Correct-by-construction specification to verified code. Ada-Europe 2017 (2017)
Petit-Doche, M., Breton, N., Courbis, R., Fonteneau, Y., Güdemann, M.: Formal verification of industrial critical software. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 1–11. Springer, Cham (2015). doi:10.1007/978-3-319-19458-5_1
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2), 156–173 (2005)
Storey, A.C., Haughton, H.P.: A strategy for the production of verifiable code using the B Method. In: Naftalin, M., Denvir, T., Bertran, M. (eds.) FME 1994. LNCS, vol. 873, pp. 346–365. Springer, Heidelberg (1994). doi:10.1007/3-540-58555-9_104
Tatibouët, B., Requet, A., Voisinet, J.-C., Hammad, A.: Java card code generation from B specifications. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 306–318. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39893-6_18
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Halchin, A., Feliachi, A., Singh, N.K., Ait-Ameur, Y., Ordioni, J. (2017). B-PERFect. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. Lecture Notes in Computer Science(), vol 10598. Springer, Cham. https://doi.org/10.1007/978-3-319-68499-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-68499-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68498-7
Online ISBN: 978-3-319-68499-4
eBook Packages: Computer ScienceComputer Science (R0)