Ansaldo STS:

  • TGV-Est ERTMS, IXL projects
  • Verification of the design models, the ADA code, safety proofs (CBTC)
  • Tools: SCADE, Polyspace

GE Transportation:

  • Projects: CBTC & ERTMS (ground and on-board)
  • Development of the verification process that includes the FHA, the proof of safety properties and the production of counter-examples
  • Tools: Simulink Design Verifier, SafeRiver Toolkit


  • Project SAET Ligne 1: verification of the B model of the on-board software, verification of the proofs (B models) and of the Data Dictionary (Safety Data)
  • Projects OCTYS and OURAGAN: independent verification of SCADE models based on the RATP proof tools
  • Tools: SCADE, Prover, Atelier B


Thales Communication and Security:

  • Project IXL Ligne 1
  • Specification and verification of the train-tracking function with Simulink Design Verifier
  • Safety-oriented verification of track data
  • Tools: ASIFER, Simulink Design Verifier, SafeRiver Toolkit