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 and run-time errors
Constitution of proof evidence with respect to the EN50128 norm (safety documents and safety analyses)
Analysis and verification of B models for CBTC systems
Verification of safety data
Development of components for cyber-security : Secured XML validator allowing a high-level of security (EAL4+) for XML data exchange, Solution customizable for various data formats and technical contexts.
Secure coding rules : JavaSec, CERT Java or Cert C, OCaml
Detection of known vulnerabilities, of hazardous instructions or patterns through static analysis
Investigation of the exploitability of detected weaknesses through static analysis or through the analysis of attack scenarios
Improvement of applications security
Safety equipments : Deployment of the ISO26262 standard at the system and software levels, Safety analysis of AUTOSAR architectures, Design and coding rules for safety, Freedom from interference (FFI) Analysis, Tool for Dependent failure analysis and FFI (IFFree).
Engine control : Compliance of control-command laws design processes with the ISO26262 standard, Compliance of the software development process with the ISO26262 standard.
Passenger compartment : Software security file for BSI platforms
X-by Wire : Study and design of a prototype for the Steer by wire