Railway Industry Development
Introduction
Prover is a thought leader in the industry actively driving innovation, shaping standards and developing best practices for efficient development and verification of rail control systems. Prover contributes to the automation and digitization of modern rail control systems through various industry organisations and forums, collaboration with Academia and driving new innovations.
Industry Associations
SDA Forum
The SDA Forum is an annual event initiated by Prover to embrace the latest evolutions of design automation and formal verification – software technologies to automate design and verification of railway signaling systems. The SDA Forum invites signaling management representatives to foster collaboration, drive standards, and to assist implementation strategies for design automation and formal verification in railways. The forum will help the industry to meet and share valuable knowledge and ideas for how to drive innovation in railway safety and more efficient software development.
Shift2Rail
Shift2Rail is the first European rail initiative to seek focused research and innovation (R&I) and market-driven solutions by accelerating the integration of new and advanced technologies into innovative rail product solutions. Shift2Rail promotes the competitiveness of the European rail industry and meets changing EU transport needs. Within Shift2Rail, Prover Technology assists Trafikverket (Swedish Transport Administration) in Technology Demonstrator (TD) 2.7, Formal methods and standardisation for smart signalling systems, and liaises with Trafikverket’s academic collaborator KTH Royal Institute of Technology.
Unife
Unife is a organisation for the European Rail Supply Industry. It also encompasses rail industry associations from 11 countries as members. Unife advocates on behalf of it´s members in Europe. Unife members are committed to collaborating on common challenges facing the railway sector. Ranging from providing innovative technologies needed to meet the growing demand for sustainable transportation, to working together to help shape interoperability standards and the coordination of EU-funded research projects that contribute to the technical harmonisation of railway systems. Prover is an active member of UNIFE contributing in relevant working groups.
HLL Forum
The HLL Forum is the community for us who use the formal specification language HLL. It is a high level language for formal verification of safety critical systems developed by Prover and RATP. As it has started to become a de facto standard, we wanted to make sure that the language develops in a controlled way to meet the demands of the future and initiated the HLL Forum. It was formed in a first meeting in Paris on December 4th 2018. Since then, tool providers have been working together to merge their different dialects of HLL into one uniform language that we aim eventually to publish as the official next version of HLL. Leading suppliers and infra strucure managers are members of the HLL Forum. The HLL-forum is focused on standardizing the HLL langugage and making it available for eveyone to use.
IEEE
Prover is a member of the IEEE Standards Association (SA) corporate program and has participated in the IEEE WG P2846 Assumptions for Models in Safety-Related Automated Vehicle Behavior (see https://sagroups.ieee.org/2846/)
CBTC User Group
Together with the metros of Copenhagen, New York City, and Stockholm, Prover has funded the CBTC User Group as a forum to exchange experiences and best practices on Communication-Based Train Control (CBTC) systems. One area of interest is the use of formal specifications as a way to maximize the benefits of investments in train control systems, and to simplify the interaction between metros and suppliers. An initial meeting with presentations from the funding members were held on March 11, 2021, and as more members join, it will be followed by quarterly meetings focusing on different topics of interest.
Innovation
AI-powered Proof Tactics, research project together with Vinnova
We have been following the latest achievements in the AI field with great interest, and after having been awarded R&D funds by Vinnova, Sweden´s Innovation Agency, we finally took the decision to move forward with the future of formal verification. AI is playing an increasingly important role in our society and life.
Our goal is to develop deep-learning models that automatically propose a good proof tactic by recognizing the high-level patterns in our customers’ HLL models. We have seen significant performance increases already and are now working on incorporating these technologies in our solutions.
LCF
LCF is a domain-specific language tailored for signaling engineering. It provides a universal way of expressing signaling configuration data in a compact and review-friendly format, to help infrastructure managers transition from drawings to structured data. LCF is a Prover innovation that we have published to in the open domain to b eused by everyone that benefits from the language. You will find the specification on HAL.
HLL
HLL is a formal high level language tailored for formal verification of industrial systems. You can automatically translate computer programs or relay systems to HLL in order to investigate them mathematically and prove properties about them with a model checker such as PSL.
With HLL you can:
- model software as a mathematical model for formal verification or simulation,
- model a software environment to investigate how the software behaves in it, and
- formally express safety requirements and lemmas.
