REFERENCES


INDUSTRIAL REFERENCES FOR ATELIER B


CLIENT : 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
> DTVT : Tool for checking the B properties on railway invariants

CLIENT : SIEMENS

> 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.
> METRO DE NEW YORK : Proof Validation OURAGAN Ligne 3.

CLIENT : RATP

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

CLIENT : CNIM

> SPRAT : Modelling the electronic architecture of a specific military vehicle

CLIENT : ATMEL

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

CLIENT : DGA

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

CLIENT : CNES

> RESEARCH : Ignition Detection
> RESEARCH : Limbs
> RESEARCH : Servogovern

CLIENT : PSA

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

CLIENT : 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