Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle - Université de Lorraine Access content directly
Theses Year : 2008

Contribution to safety requirements verification : application to industrial machinery domain

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

Dominique Evrot
  • Function : Author
  • PersonId : 760666
  • IdRef : 135649579

Abstract

Introduction of new information and communication technology in automated systems leads to a growth of safety functions complexity. System properties are not limited to components properties, they issued from an interactions network that can introduces bad behaviour. Our conviction is that a safe development of such system must involve system oriented approaches in order to apprehend system global behaviour and architecture and more formal approaches allowing verifying that components properties satisfy end users system requirements We define a methodological approach based on SysML formalism (System Modelling Language) allowing global system requirements identification; formalisation and structuring in order to project these requirements on the system components architecture and so obtain local components properties. Then safety requirements verification is based in one hand on proved refinement (using theorem proving) of system requirements to components properties; and, in the other hand, on the formal verification (using model checking) of these components properties.
L'introduction des nouvelles technologies de l'information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu'ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d'un réseau d'interactions entre ces constituants qui peut être à l'origine de comportements néfastes et difficiles à prévoir. Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées « système », qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s'assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences « système » formulées par les utilisateurs. Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l'identification, la formalisation et la structuration d'exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d'une part, sur un raffinement prouvé (par theroem proving) des exigences « système » permettant d'établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d'autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.
Fichier principal
Vignette du fichier
SCD_T_2008_0038_EVROT.pdf (2.04 Mo) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

tel-01748464 , version 1 (29-03-2018)

Identifiers

  • HAL Id : tel-01748464 , version 1

Cite

Dominique Evrot. Contribution à la vérification d'exigences de sécurité : application au domaine de la machine industrielle. Autre. Université Henri Poincaré - Nancy 1, 2008. Français. ⟨NNT : 2008NAN10038⟩. ⟨tel-01748464⟩
49 View
219 Download

Share

Gmail Mastodon Facebook X LinkedIn More