Home - News - Products - Versions - Download - Manuals - Maintenance - Distribution Policy - Roadmap & Contribution - Support - Training - Documents - Press - References - R&D - Contacts - Jobs - Links - Your Account 

Industrial References for Atelier B

ClearSy References
Client Domaine d'Intervention

Alstom
  • URBALIS EVOLUTION : Modelling, creation and formal proof (B method) of the SIL 4 on-board software for the new Peking underground commissioned for the 2008 Olympic Games: energy and location control. In addition creation of a safety tool for the generation of railway data that configures the on-board software.
  • URBALIS 200: Development of a safety (SIL4), validation and integration application for undergrounds in Santiago, Madrid, Seoul and Delhi
  • URBALIS 300: Development of a safety (SIL4), validation and integration application for undergrounds in Singapore and Lausanne

 

Atmel
  • Several modelling projects for a smart card security policy at a Common Criteria EAL5+ certification level

 

CNES
  • RESEARCH: Ignition Detection
  • RESEARCH: Limbs
  • RESEARCH: Servogovern

 

CNIM
  • SPRAT : Modelling the electronic architecture of a specific military vehicle

 

DGA
  • OISAU: Study based on the creation of a requirement specification for a new standard concerning the opening and interoperability of autonomous systems

 

PSA
  • BR-VV : Modelling of the operating principles for 3 car models.

 

RATP
  • DOF1 : System modelling, safety software development
  • COPPILOT : System modelling, safety software development
  • COPP : System modelling, safety software development
  • OVADO: Tool for checking the B properties on railway invariants

 

STS
  • TRAINGUARD: Participation in the B development of the CBTC Trainguard product
  • BARCELONE BORD: Safety software B development for the Barcelona underground
  • VAL DE ROISSY: Development of the following software, according to B method: creation of the formal general design (requirements) and the formal detailed design (algorithm and code); mathematical proof of coherence, refinement and coding.
  • NEW YORK UNDERGROUND: Proof Validation
  • OURAGAN Ligne 3

STMICROELECTRONICS
  • FORCOMENT: Modelling of micro-electronic components
  • L4B4 : Development of a micro-kernel
  • PHENIX : Modelling of a smart card security policy at a Common Criteria EAL5+ certification level