Une approche classique pour les systèmes critiques consiste à avoir des mécanismes de surveillance indépendants de la chaîne de commande principale, visant à empêcher l’occurrence de défaillances catastrophiques. Ces mécanismes mettent en œuvre des vérifications en ligne, et déclenchent des interventions de sécurité lorsqu’une situation dangereuse est observée. Une telle approche a déjà été adoptée pour des systèmes autonomes, mais la spécification des règles de sécurité (quelle intervention lancer ?, quand ?) est typiquement ad hoc. De plus, les moniteurs de sécurité existants ne considèrent qu’un ensemble très limité d’interventions telles qu’une coupure d’alimentation irréversible. Une motivation pour nos travaux a été de développer une approche formelle pour la spécification des règles de sécurité, et de pouvoir prendre en compte un ensemble plus riche d’interventions temporaires, pouvant être activées et désactivées selon l’état du système. Tout en assurant la sécurité, les règles doivent être suffisamment permissives pour que le système puisse remplir ses fonctions. Par exemple, un robot mobile doit toujours garder la possibilité d’atteindre des états où sa vitesse est non nulle, permettant ainsi sa fonction de déplacement.

La méthode SMOF (Safety Monitoring Framework), et l’outil support de même nom, ont été développés pour répondre à ces besoins[1]. La méthode démarre par une analyse de risque de type HAZOP, et utilise des techniques de vérification formelle pour synthétiser les règles de sécurité. L’algorithme de synthèse prend en compte à la fois des exigences de sécurité et de permissivité (ces dernières étant des propriétés d’atteignabilité dans l’espace d’état). Le principe est d’associer des interventions à des états d’alerte, c’est-à-dire des états nécessairement traversés avant la violation d’un invariant. L’exploration des associations états d’alerte/interventions s’effectue selon un algorithme de branch and bound, qui fait des appels au model checker NuSMV pour vérifier des critères de coupe ou confirmer l’obtention d’une solution sûre et permissive. Une mise en œuvre alternative faisait appel à la notion de jeu formel entre le moniteur de sécurité et un adversaire, mais elle n’a pas été retenue pour des raisons de performance[2]. L’outil support fournit un patron de modélisation NuSMV pour faciliter la définition des comportements non sûrs en l’absence du moniteur et proposer des interventions candidates avec leurs pré-conditions et effets. Les états d’alerte sont automatiquement identifiés en tant que prédécesseurs des états catastrophiques.

L’outil offre également une aide pour produire des propriétés de permissivité. Par défaut, il considère des propriétés d’atteignabilité génériques , mais l’utilisateur peut aussi modéliser des propriétés spécifiques aux besoins de l’application[3]. Cette possibilité est très utile en pratique, car l’absence de solution provient souvent de la difficulté à maintenir la permissivité générique, qui est très exigeante. Une extension récente concerne l’ajout d’une aide au diagnostic, pour l’analyse des règles de sécurité sûres mais insuffisamment permissives. Enfin, nous avons étudié comment suggérer automatiquement de nouvelles interventions à injecter dans le processus de synthèse, pour résoudre ces problèmes de permissivité.

SMOF a été appliqué à différents robots développés par des partenaires industriels : un robot manufacturier (Kuka), un robot de maintenance sur site aéroportuaire (Sterela), et un robot agricole pour l’alimentation de bétail (Kuhn).

[1] Machin M., Guiochet J., H. Waeselynck, Blanquart J-P. , Roy M.,Masson  L., “SMOF - a Safety Monitoring Framework for Autonomous Systems”, IEEE Transactions on Systems, Man, and Cybernetics: Systems, Vol. 48, no. 5, pp. 702-715, 2018

[2] Machin M., Dufossé F., Guiochet J., Powell D., Roy M., Waeselynck H.,”Model-checking and Game Theory for the Synthesis of Safety Rules”, 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015), Daytona Beach, Florida, USA, 2015

[3] Masson L., Guiochet J., Waeselynck H., Cabrera K., Cassel S., Törngren M., “Tuning Permissiveness of Active Safety Monitors for Autonomous Systems”, Tenth NASA Formal Methods Symposium (NFM 2018), Springer LNCS 10811, pp.333-348, 2018