Conception de systèmes embarqués critiques multi-domaines respectant les normes de Sûreté Industrielle (SIL, DAL)


- par Eric Bonnafous et Sébastien Heim -


CS fait partie du comité de pilotage du projet DEPARTS (DEsign PAtterns for Real-Time and Safe applications) qui vise à développer un environnement intégré de conception de systèmes embarqués critiques multi-domaines respectant les normes de Sûreté Industrielle (SIL, DAL). Le projet issu d’un appel à projet BGLE (Brique Générique Logiciel Embarqué) est guidé par des cas d’utilisation industriels fournis par NEXTER, SNCF, EDF et CNES lanceurs.
                                                                    
Parmi les produits issus de ce projet, CS, en collaboration avec des experts académiques de l’ENSTA Bretagne, s’attache à fournir une Brique de Vérification Formelle (BVF) qui complète l’environnement intégré de conception.

L’objectif de cette brique est de fournir à l’ingénieur concepteur de systèmes embarqués critiques les moyens d’apporter la preuve du bon comportement du système conçu versus des propriétés sensibles à garantir. Pour cela cette brique fait appel aux techniques dites de Model-checking. Ces techniques associées aux méthodes et outils développés en commun par CS et L’ENSTA Bretagne depuis bientôt huit années nous ont conduit à proposer la brique BVF dans le cadre de ce projet.                                                          

Nos travaux consistent à mettre en place une approche de vérification formelle, basée sur des modèles de spécification et de conception. Cette démarche s’applique donc sur les phases amonts du cycle de développement (avant génération de code source), et se décompose en phases :
  • Formaliser les exigences (textuelles) de spécification sous forme de propriétés et de contextes d’exécution,
  • Modéliser la partie applicative du système à l’aide d’un langage métier (tel que SysML, SCADE, SDL),
  • Transformer ce modèle utilisateur en langage formel et le composer avec les propriétés de la plate-forme,
  • Vérifier le comportement du système à l’aide d’un model-checker (de manière exhaustive pour chaque contexte donné).

Initialement conçue pour apporter la preuve de bon fonctionnement de propriétés pour des environnements de modélisation de type asynchrone (langages type SDL et SysML/UML), CS définit les conditions d’emploi de ces techniques dans un environnement de modélisation de type synchrone (langage type LUSTRE (= SCADE)) largement utilisé dans l’industrie des systèmes embarqués critiques.

L’originalité des techniques mises en œuvre pour atteindre l’objectif visé repose sur :
  • la notion de contexte qui permet de limiter la portée d’une propriété aux seuls modes de fonctionnement pour lesquels cette propriété est présente,
  • la mise en œuvre de techniques évoluées de réduction basées sur :
    • le dépliage de Contextes
    • des Algorithmes d’optimisation (PastFree)
    • des explorations distribuées sur réseau
et plus spécifiquement pour les modèles synchrones à l’application du concept GALS (Globally Asynchronous Locally Synchronous).
 
In fine, l’approche outillée par BVF nous permettra de caractériser le comportement de l’enchainement d’un ensemble de planches SCADE tout en prenant en compte les contraintes de la plateforme (scheduling, ordonnancement) ce qui représente une avancée conséquente par-rapport aux besoins actuels de l’industrie.

A noter qu’il existe d’autres méthodes et outils pour vérifier la précision de calculs flottants, et analyser l’ordonnancabilité globale.                                                                           

Les premiers essais se sont avérés concluants et nous ont permis de valider la faisabilité de l’approche sur un modèle Scade d’un Cruise Control. Un essai sur un modèle Scade industriel est en cours.
 
Ces résultats nous ont naturellement amenés à présenter à la conférence ERTS2 2016 un article sur le sujet intitulé : " Model Checking of Scade Designed Systems" dont les proceedings se retrouveront sur le site http://hal.archives-ouvertes.fr/ERTS2016.
 

 


Des centres d'excellence technologiques