Publié le 14 septembre 2011

Références Industrielles de l’Atelier B

 

 
Client Domaine d’Intervention
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 (SIL4), validation et intégration pour les métros de Santiago, Madrid, Seoul, et Delhi.
  • URBALIS 300 : Développement d’une application sécuritaire (SIL4), validation et intégration pour les métros de Singapour et Lausanne

 

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

 
CNES
  • RECHERCHE : Détection Allumage
  • RECHERCHE : Limbes
  • RECHERCHE : Servogouverne

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

 
DGA
  • OISAU : Etude portants 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

 
PSA
  • BR-VV : Modélisation des principes de fonctionnements de 3 modèles de voiture

 
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
  • OVADO : Outil de Vérification de propriétés B sur les invariants ferroviaires

 
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

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+

Les commentaires sont fermés.