Validation formelle système

La vérification formelle de système, obtenue avec la méthode B, est un élément de la démonstration de sûreté de fonctionnement d’un système critique. 

CLEARSY utilise dans son mode opératoire la description détaillée de la conception et des algorithmes employés au sein du système analysé. Les modèles B développés à partir de ces éléments contiennent:

• la formulation mathématique des propriétés voulues,
• la formulation mathématique de toutes les hypothèses nécessaires et
• les éléments de conduite de preuve.

Une fois ces modèles prouvés avec l’Atelier B, nous avons donc la garantie que les propriétés voulues découlent mathématiquement des hypothèses sélectionnées. Ces hypothèses constituent donc toutes les conditions suffisantes pour garantir logiquement les propriétés voulues. Ces conditions concernent la conception, le matériel et le contexte.

Ce processus nécessite la compréhension fine du véritable « pourquoi » de la sécurité, obligeant ainsi des échanges forts avec les experts métiers concernés. 

CLEARSY a par exemple procédé à la vérification système avec preuve du CBTC de la ligne 7 de New York, avec la méthode B.

Les propriétés système prouvées ont été:
> L’impossibilité de collision entre trains
> L’impossibilité de déraillement sur aiguille déverrouillée
> L’impossibilité de survitesse