Prover Diagnostic

Hazard-based formal verification that challenges safety mitigations before deployment

Prover Diagnostic is a packaged, hazard-based formal verification solution that helps identify and eliminate potential safety risks early – before they become costly or difficult to change.


Instead of only verifying that requirements are implemented as written, Prover Diagnostic asks a tougher question: Are your mitigations actually sufficient to prevent hazardous states?

At a glance: Inputs and outputs

  • Inputs

    • Hazard Log (system hazards and mitigations)
    • SRACs (safety-related constraints and operational assumptions)
    • A formal model of the software logic (generated or imported from an existing design)

  • Outputs

    • Proof results showing hazardous states are unreachable in the formal model, under stated assumptions, or
    • Clearly reported counterexample scenarios that explain how a hazardous state can be reached
    • A structured report that can support the Technical Safety Report (TSR) and the Safety Case

Request a proposal (customer-specific scope and pricing)

prover diagnostic

I’m interested in Prover Diagnostic

Start strengthening your safety assurance; fill out the form to learn more.

SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
Hitachi Rail STS
Alstom
New York City Transfer
Siemens
Thales
SL
Infrabel
RATP
SWECO
Canadian Pacific
Trafikverket
ATKINS
Hitachi Rail STS
Alstom
New York City Transfer
Siemens
Thales

What makes Prover Diagnostic different?

Formal verification is often requirements-driven, tracing properties back to safety requirements. This approach supports testing (TST) and verification (VER) teams through exhaustive exploration using the Prover PSL proof engine, aligned with CENELEC norms.

Prover Diagnostic takes a different angle: it supports the Safety Assurance team by deriving safety properties directly from system hazards and the Hazard Log, introducing automation into a part of safety assessment that has traditionally been manual.

This provides an independent and complementary way to challenge mitigations, strengthening functional safety analyses with objective, model-based evidence.

How Prover Diagnostic works

Integration obstacles

1) Identify safety properties from hazards

Safety properties are modeled from system hazards, such as:

  • collision scenarios
  • derailment scenarios

This ensures direct traceability between identified hazards and the formal properties used to challenge the design.

2) Define an environment model and constraints (SRACs)

An environment model captures safety-related constraints of:

  • wayside components (e.g., switch machines)
  • interfacing subsystems
  • operational procedures

For example, the environment model can ensure that a switch cannot change position unless it has been commanded or manually operated.

Formal verification signaling issues

3) Analyze the software logic using formal proof

These elements are used to analyze a formal model of the logic (automatically generated or imported from an existing design).

The analysis exhaustively explores the modeled behaviors under defined assumptions and constraints. Hazardous states are either proven unreachable within the model or reported with a scenario that supports review and targeted improvement.

Why choose Prover Diagnostic?

Independent challenge of safety measures

Mitigations are challenged against a formal model – not only engineering judgement or test coverage – helping reveal gaps that traditional reviews may miss.

Exhaustive exploration of modeled behaviors

The Prover PSL proof engine enables exhaustive coverage of the modeled functional behaviors, without relying on “did we think of the right test case?”

Stronger, clearer Safety Case

Findings and hypotheses are documented in a way that fits naturally into the TSR, supporting compliance with CENELEC norms and making assessments easier to defend.

Reduced late rework and project risk

Unsafe scenarios are exposed earlier, with precise counterexamples that guide targeted improvements instead of broad redesign.

Better alignment between hazards and design

Because properties are derived from the Hazard Log, you gain assurance that the implemented logic supports functional safety analyses and the system-wide risk picture.

Book a meeting

Get a customer-specific proposal for Prover Diagnostic

Share a few details about your project and we will get back to discuss scope, inputs, and expected deliverables.

Typical inputs include:

  • Hazard Log
  • SRACs/operational constraints
  • A model of the software logic

I’m interested in a Prover Diagnostic. Contact me!