OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

B-PERFect - Applying the PERF Approach to B Based System Developments

Halchin, Alexandra and Feliachi, Abderrahmane and Singh, Neeraj Kumar and Aït-Ameur, Yamine and Ordioni, Julien B-PERFect - Applying the PERF Approach to B Based System Developments. (2017) In: International Conference Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail 2017), 14 November 2017 - 16 November 2017 (Pristoia, Italy).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/978-3-319-68499-4_11


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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in volume 10598 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN: 978-3-319-68499-4 The original PDF is available at: https://link.springer.com/chapter/10.1007%2F978-3-319-68499-4_11
HAL Id:hal-02451007
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Régie Autonome des Transports Parisiens - RATP (FRANCE)
Laboratory name:
Deposited On:16 Jan 2020 10:25

Repository Staff Only: item control page