Contribution à la vérifiction d'exigences de sécurité : application au domaine de la machine industrielle

Les installations automatisées font maintenant couramment appel à des automates programmables pour traiter des fonctions assurant la sécurité des personnes. Ceci impose de prendre en compte la sûreté des logiciels intégrés dans ces automates, donc les erreurs susceptibles de les affecter. Cette préoccupation nécessite de mettre en œuvre des méthodes de conception pour éviter d'introduire ces erreurs et pour augmenter la confiance dans les performances de ces installations.
Cette étude explore une des possibilités de conception du logiciel qui consiste à combiner les pratiques classiques telles que le test par simulation mises en œuvre par les automaticiens avec les techniques de vérification formelles issues du génie logiciel. Ces dernières, non utilisées actuellement dans le domaine de la machine, permettent de garantir qu’une exigence de sécurité est vérifiée à 100% et donc que la partie du logiciel réalisant cette exigence ne contient plus d’erreurs risquant de compromettre la sécurité de l’opérateur. Ces techniques ont des limitations et nécessitent, pour être appliquées dans le domaine de la machine, le suivi d’un processus de développement particulier.
Un processus de développement, focalisé sur les aspects sécurité, est donc proposé. Il débute par l’expression des besoins du système afin d’aboutir à un ensemble d’exigences de sécurité. Cette partie a pour intérêt de formaliser et de tracer les exigences de sécurité à partir d’une démarche globale d’analyse des risques alors que, dans le monde de la sécurité machine, ces aspects ne sont pas forcément pris en compte dès le début de la conception. Ces exigences sont ensuite utilisées pour coder le logiciel du système puis pour le valider. Cette validation pourra se faire, en fonction de la maturité, de la compétence et des moyens mis en œuvre par le concepteur, soit par simulation, soit à l’aide des techniques de vérification formelle.