CLEARSY a développé et certifié la CLEARSY SAFETY PLATFORM (CSP), une solution pour développer des systèmes embarqués temps réel sécuritaires certifiés jusqu’au niveau SIL4. La CSP fournit un cadre, basé sur la méthode formelle B, pour garantir les propriétés de sécurité au niveau logiciel. Ce cadre comprend un IDE dédié, une documentation détaillée et des exemples d’application.
Les propriétés de sécurité de l’application sont formalisées dans des modules de spécification dédiés, incluant éventuellement le comportement de l’environnement. Les modules intègrent également l’implémentation logicielle de leur spécification. Grâce à la méthode B, il est possible de prouver formellement que ces implémentations sont conformes à 100% à leur spécification. La CSP inclut une bibliothèque, également développée en B, fournissant les éléments pour exprimer des propriétés de sécurité sur l’exécution du logiciel. En particulier, les propriétés temporelles peuvent être formalisées et prouvées.
L’IDE CSP fournit un processus de double compilation entièrement automatique qui génère un exécutable binaire et le télécharge sur la plateforme CSP. Cet exécutable est garanti pour exécuter fidèlement le logiciel développé ou pour retomber dans un état vital stable, dès lors que les conditions d’une exécution sûre ne peuvent être garanties.
En combinant l’assurance de la méthode B sur le développement logiciel et l’assurance de la CSP sur la compilation/exécution, CLEARSY a construit un cadre complet de développement logiciel, des propriétés de sécurité de haut niveau à l’exécution embarquée de bas niveau.
En adoptant la plate-forme CSP, les développeurs sont libérés de la gestion compliquée des défaillances matérielles et concentrent leurs efforts sur la spécification des fonctionnalités et des propriétés de sécurité souhaitées, et sur la conception d’une solution qui réalise cette spécification. Les autres étapes sont entièrement automatiques et prises en charge par les outils certifiés et par l’unité de traitement vitale certifiée CSP.
Cadre de développement CSP :
– Développement de logiciels certifiés
– Processus de compilation certifié
– Exécution certifiée
– Certificat générique et règles à appliquer pour l’environnement
Il s’agit d’un grand pas en avant dans l’extension du paradigme de la méthode B : « Assigning program to meanings ».
« Assigning safe processing to meanings » est le résultat de plus de 25 ans d’expérience de CLEARSY dans l’application de méthodes formelles et la conception de systèmes critiques de sécurité.