LES RÉFÉRENCES


RÉFÉRENCES INDUSTRIELLES DE L'ATELIER B


CLIENT : ALSTOM

> URBALIS EVOLUTION : Modélisation, réalisation et preuve formelle (méthode formelle B) du logiciel embarqué SIL 4 du nouveau métro de Pékin mis en service pour les jeux Olympiques 2008 : contrôle d’énergie et localisation. Réalisation également d’un outil sécuritaire de génération des données ferroviaires qui paramètrent le logiciel embarqué.
> URBALIS 200 : Développement d’une application sécuritaire (SIL 4), validation et intégration pour les métros de Santiago, Madrid, Séoul et Delhi.
> URBALIS 300 : Développement d’une application sécuritaire (SIL 4), validation et intégration pour les métros de Singapour et Lausanne.
> DTVT : Outil de vérification de propriétés B sur les invariants ferroviaires.

CLIENT : SIEMENS

> TRAINGUARD : Participation au développement B du produit CBTC Trainguard.
> BARCELONE BORD : Développement B logiciel sécuritaire du métro de Barcelone.
> VAL DE ROISSY : Développement selon la méthode formelle B des logiciels : réalisation de la conception générale formelle (exigences) et de la conception détaillée formelle (Algorithmes et code); Preuve mathématique de cohérence, de raffinement et de codage.
> METRO DE NEW YORK : Validation de preuve OURAGAN Ligne 3.

CLIENT : RATP

> DOF1 : Modélisation système, développement logiciel sécuritaire.
> COPPILOT : Modélisation système, développement logiciel sécuritaire.
> COPP : Modélisation système, développement logiciel sécuritaire.
> Outil de vérification de propriétés B sur les invariants ferroviaires.

CLIENT : CNIM

> SPRAT : Modélisation de l’architecture électronique d’un véhicule militaire spécifique.

CLIENT : ATMEL

> Plusieurs projets de modélisation d’une politique de sécurité pour carte à puce d’un niveau de certification Critères Communs EAL5+.

CLIENT : DGA

> OISAU : Étude portant sur la réalisation d’une spécification de besoin d’un nouveau standard concernant l’ouverture et l’interopérabilité des systèmes autonomes.

CLIENT : CNES

> RECHERCHE : Détection Allumage
> RECHERCHE : Limbes
> RECHERCHE : Servogouverne

CLIENT : PSA

> BR-VV : Modélisation des principes de fonctionnement de 3 modèles de voiture.

CLIENT : STMICROELECTRONICS

> FORCOMENT : Modélisation de composants micro-électroniques
> L4B4 : Développement d’un micro-kernel
> PHENIX : Modélisation d’une politique de sécurité pour carte à puce d’un niveau de certification Critères Commun EAL5+