Qualification of a Formal Data Consistency Verification Tool
| Success Story|
|Keywords||EventB, formal tool, IEC-50128|
|Credit||University of Düsseldorf, Formal Mind|
Helped with University of Düsseldorf, Siemens developed a tool leading to a tremendous Productivity Improvement of Data Consistency in Transportation Models. However as this tool is part of a validation chain of a critical system, it is subject to certification constraints.
More precisely, safety-critical systems in transportation have to comply with IEC-50128 standard which is derived from the generic IEC61508 standard. Following the 2011 revision of the norm, the tool is classified as class T2 (not impacting code but part of the V&V chain) and the selection of the tools of this ckass must be adequately justified, including the identification of potential failures which can be injected into the tools output and the measures to avoid or handle such failures.
Of Interest to the High Level Manager
- getting a new tool accepted requires convincing arguments, especially when it involves a radical change of tooling technology. This successfull demonstration opens the way to a larger adoption. Actually, since this success story, similar techniques are already being applied in other domaisn such as aeronauticss, see Formal Data Validation of Flight Configuration Data
- During the systematic process of producing the required evidence resulted in the improvement of the tooling architecture (e.g. isolation of ProB modules involved in the tool chain, versioning) and also to the discovey of errors hidden in the build chain (e.g. compiler bugs).
- there is feedback available on this validation report by the certification authority
The following strategies were used to increase the confidence in the proper working for ProB on the STS property validation task and provide the required qualification evidence
- Repeated successful application on case studies, discovering all known problems as well as in one case discovering unknown problems in the properties.
- Extensive regression, unit-tests, automated unit-test generation, and validation via mathematical laws and model checking; which have even discovered several errors in the underlying compiler.
- Coverage analysis of the testing, ensuring that all critical parts are covered by the tests; this has enabled us detecting a few more issues (and has prompted us to develop the automated unit-test generator)
- Validation of the parser and type-checker via pretty-printing and cross-checking with the Atelier-B parser (bcomp). The internal representation of ProB for a particular Siemens model can be fed at runtime to bcomp, for additional validation that the type inference was properly conducted.
- Double evaluation of predicates, to catch undefined predicates as well as errors in the ProB kernel and interpreter relating to predicates.
Although AtelierB is still used for the typechecking part, the ProB-based validation tool is now in use and especially for the certified Roissy and PAR1 lines.
Specific DEPLOY Contributions
- University of Düsseldorf and its Formal Mind spin-off contributed the certification report and some original and efficient way of producing strong evidence of correctness (such as double evaluation of predicates and automated test generation)
- ↑ Leuschel, Michael and Falampin, Jérôme and Fabian, Fritz and Daniel, Plagge Automated Property Verification for Large Scale B Models. In: Proceedings FM 2009. Springer-Verlag, Eindhoven, the Netherlands, November 2-6, 2009
- ↑ Industrial deployment of system engineering methods providing high dependability and productivity. A. Romanovsky, M. Thomas (Eds). Springer. 2012