Jury

• Janan ZAYTOON, Professor at Université de Reims, Président
• Hassane ALLA, Professor at Université de Grenoble, Reviewer
• Thierry JÉRON, Research Director at l'INRIA Rennes, Reviewer
• Franck CORBIER, Doctor Ingeneer R&D Geensoft/Dassault Systèmes, Examiner
• Jean-Marc FAURE, Professor at SUPMECA, Supervisor
• Jean-Marc ROUSSEL, Associate Professor at ENS Cachan, Co-supervisor

Keywords: Conformance test, Grafcet, Logic controllers, Programmable Logic Controller, Model transformation, SIC-testability

Abstract

The works presented in this PhD thesis deal with the generation and implementation of test sequences for conformance test of logic controllers. Within these works, Grafcet (IEC 60848 (2002)), graphical specification language used in industry, has been selected as the specification model. Logic controllers mainly considered in these works are Programmable Logic Controllers (PLC). In order to validate the carrying out of conformance test of critical control systems, this thesis presents :

• A formalization of the Grafcet specification language. Indeed, to apply usual verification and validation methods, the behavior is required to be expressed through formal models. However, in industry, the models used to describe functional specifications are chosen for their expression power and usability, but these models rarely have a formal semantics.
  

• A study of test sequences execution and analysis of obtained verdicts when several logical inputs are changed simultaneously. Series of experimentation have permitted to quantify, for different configurations of the implantation under test, the rate of erroneous verdicts due to these simultaneous changes.

• A definition of the SIC-testability criterion for an implantation. This criterion, determined on the Grafect specification defines the ability of an implementation to be tested without any erroneous verdict. Automatic generation of test sequences that minimize the risk of erroneous verdict is then studied.