From Fault Tree Analysis to Model Checking of Logic Controllers
| Authors: | Barragan Santiago Israel, LURPA, France, Metropolitan
Faure Jean-Marc, LURPA, France, Metropolitan |
|---|
| Topic: | 5.1 Manufacturing Plant Control |
|---|
| Session: | Dependable Manufacturing Systems Control II |
|---|
| Keywords: | Dependability, Fault forecasting, Fault removal, Fault tree analysis, Formal verification, Temporal logic |
|---|
Abstract
This paper proposes a method enabling to state formal properties of a logic controller, a prerequisite for formal verification using model-checking, from a fault-tree analysis taking into account both the controlled process and the controller. Invariants, untimed and timed properties are considered and illustrated thanks to an example. The aim of this method is to ease formal properties design and to bridge the gap between fault forecasting and fault removal for automated systems
