Verification of system principles and designs with the help of formal methods and proofs

  • CBTC (train tracking, anticollision, odometry, speed control), PMI (proof of conformance with policies, configuration), Signalling, ERTMS

Analysis and verification of Simulink/SCADE models for CBTC systems

  • Functional safety requirements & run-time errors

Analysis and verification of B models for CBTC systems

Verification of safety data

Analysis of the conformance of the software requirements with respect to system safety requirements

Code analysis (RTE, value/domain analysis, robustness analysis)

Constitution of proof evidence with respect to the EN50128 norm (safety documents, safety analyses)