Advertisement

Interlocking Design Automation Using Prover Trident

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

This article presents the industrial-strength Prover Trident approach to develop and check safety-critical interlocking software for railway signaling systems. Prover Trident is developed by Prover Technology to meet industry needs for reduced cost and time-to-market, by capitalizing on the inherent repetitive nature of interlocking systems, in the sense that specific systems can be created and verified efficiently as specific instances of generic principles. This enables a high degree of automation in an industrial-strength toolkit for creation of design and code, with seamless integration of push-button tools for simulation and formal verification. Safety assessment relies on formal verification, performed on the design, the revenue service software code as well as the binary code, using an independent toolset for formal verification developed to meet the applicable certification requirements. Basic ideas of this approach have been around for some time [1, 2, 3], while methodology and tools have matured over many industrial application projects. The presentation highlights the main ingredients in this successful application of formal methods, as well as challenges in establishing this approach for production use in a conservative industry domain.

Keywords

Formal verification Sign-off Interlocking Prover trident 

References

  1. 1.
    Borälv, A.: Case study: formal verification of a computerized railway interlocking. Formal Aspects of Comput. 10, 338 (1998).  https://doi.org/10.1007/s001650050021CrossRefMATHGoogle Scholar
  2. 2.
    Borälv, A., Stålmarck, G.: Formal verification in railways. In: Hinchey, M.G., Bowen, J.P. (eds.) Industrial-Strength Formal Methods in Practice. Formal Approaches to Computing and Information Technology (FACIT), pp. 329–350. Springer, London (1999).  https://doi.org/10.1007/978-1-4471-0523-7_15CrossRefGoogle Scholar
  3. 3.
    Duggan (Siemens), P., Borälv, A.: Mathematical Proof in an Automated Environment for Railway Interlockings, Technical Paper in IRSE Presidential Programme, IRSE NEWS 217 (2015)Google Scholar
  4. 4.
    Layout Configuration Format (LCF) v1.1, Format Specification. PCERT-LCF-FMT, version 1.0, Prover Technology (2018)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Prover TechnologyStockholmSweden

Personalised recommendations