Simplified interlocking application engineering with Prover iLock for NEAT’s GeminiX platform

Prover and NEAT are together demonstrating the benefits of using the Prover iLock tool suite for engineering interlocking applications executed on NEAT’s GeminiX platform. GeminiX is a SIL-4 generic product consisting of a real-time OS, redundant CPUs, and I/O modules. Prover iLock is a desktop tool for producing fully documented, tested and verified application software for railway signaling systems.

The demonstration includes:

• The Prover iLock process for generating the interlocking logic from generic specifications and graphical configuration data, with
  • simulation-testing based functional testing,
  • formal safety verification, and
  • generation of C-code for execution on the GeminiX platform.
• Execution on the GeminiX platform:
  • cross-compilation and execution of the generated C-code using a dedicated SIL-4 task on GeminiX-OS,
  • configuration of I/O, and
  • connection to Prover iLock for real-time hardware in the loop testing, with visualization of generated test cases and manual interaction.

The safe function of the generated application logic (C-code) can be formally verified with the SIL-4 T2 sign-off verification tool Prover Certifier, certified by TÜV Nord.

The demonstration has been set up in NEAT’s lab, with the GeminiX hardware connected to Prover iLock via a communication link, to provide simulation of wayside objects and a control panel, as shown in this video:

Highlights of the GeminiX platform include:

• A complete Platform Documentation Package and Application Conditions, which describe and certify the compliance for applications up to SIL4 according to the EN50126/128/129 and IEC61508 standards.
• A HW 2oo2 diverse reference architecture, that can be made redundant for reliability.
• A real-time OS-like environment, GeminiX–OS, certified as a SIL4 Generic Product on its own and also certified several times into clients’ products. It is independent from the specific hardware, and includes its own complete Documentation Package.
• A VHDL Source Code, which implements diagnostic routines and generic I/O, independent from the specific hardware, certified as a SIL4 Generic Product.
• Several Reference Designs, implemented using different CPUs (Intel, AMD, ARM, …) and different bus architectures.

Signaling Design Automation with Prover iLock is a more efficient approach to develop rail control software, rooted in an engineering process based on formal methods, modelling, and automation. In addition to enhancing the development process, it also paves the way for standardization and more open system, something that is key to drive down the long-term costs for rail control. With a development process that is not tied to a specific signaling vendor, the rail infrastructure managers can get in control of the life-cycle of their systems, and can address issues such as obsolescence with more flexibility. The combination of Signaling Design Automation with the GeminiX platform is a good example of how these benefits can be realized for an interlocking system.

Prover and NEAT will showcase their joint solution later this year at InnoTrans and you are also welcome to request a demonstration online or onsite. Please come visit NEAT and Prover at InnoTrans in Berlin, September 24-27, 2024. You will find NEAT in Hall 27, stand 140 and Prover in Hall 3.2, stand 130. Looking forward to seeing you there!

To learn more about signaling design automation with Prover iLock please visit www.prover.com, and more information on the GeminiX platform is available at www.neat.it or www.geminix.com.