Expert systèmes critiques

Atelier B et preuve


L’atelier B développé par l’entreprise Clearsy se fonde sur la méthode formelle de développement logiciel B.
Il s’agit d’un processus de développement logiciel qui part d’une spécification formatée en langage mathématique B, le modèle abstrat, pour arriver au code par raffinements successifs, en finissant par le transcodage en C ou Ada.
Les propriétés fondatrices du modèle abstrait, puis les raffinements successifs, sont prouvés à l’aide du prouveur de l’atelier B. Le prouveur s’établit sur une base de règles, axiomes mathématiques à la base des lemmes prouvés.
Le code obtenu est donc couvert par la preuve et la certification de l’atelier, des règles et du traducteur en C ou Ada.
Ceci permet de s’économiser la plupart des tests du système. En fait, seules les entrées/sorties ont besoin d’être testées.