Formal and Joint Verification of Control ...
Document type :
Communication dans un congrès avec actes
Title :
Formal and Joint Verification of Control Programs and Supervision Interfaces for Socio-technical Systems Components
Author(s) :
Mesli, Soraya [Auteur]
ArchWare
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
Toguyéni, Armand [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Bignon, Alain [Auteur]
Segula Technologies [France]
Oquendo, Flavio [Auteur]
ArchWare
Kesraoui, Djamal [Auteur]
Segula Technologies [France]
Berruet, Pascal [Auteur]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
ArchWare
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
Toguyéni, Armand [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Bignon, Alain [Auteur]
Segula Technologies [France]
Oquendo, Flavio [Auteur]
ArchWare
Kesraoui, Djamal [Auteur]
Segula Technologies [France]
Berruet, Pascal [Auteur]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
Conference title :
Proceedings of the 13th IFAC Symposium on Analysis, Design, and Evaluation of Human-Machine Systems (HMS 2016)
City :
Kyoto
Country :
Japon
Start date of the conference :
2016-08-30
Book title :
Journal IFAC PapersOnLine (Elsevier)
Publisher :
IFAC
English keyword(s) :
Formal Verification
Control-Command
HMI
Model Checking
CTL
Control-Command
HMI
Model Checking
CTL
HAL domain(s) :
Informatique [cs]/Génie logiciel [cs.SE]
Sciences de l'ingénieur [physics]
Sciences de l'ingénieur [physics]
English abstract : [en]
The Anaxagore Project provides a component-based design ow for reconfigurable socio-technical systems. Each component integrates a control program and a supervision interface and it has been validated by empirical testing. ...
Show more >The Anaxagore Project provides a component-based design ow for reconfigurable socio-technical systems. Each component integrates a control program and a supervision interface and it has been validated by empirical testing. The purpose of this paper is the use of formal methods for the verification of the whole component control-command chain. Different component features (the control program, the supervision interface, the physical device) and the human tasks are modeled using timed automata. These timed automata are then checked by model checking (UPPAAL) with a set of safety and usability properties written in CTL. Our approach is presented through an industrial case study: the supervised control of a 2-way motorized valve. The results show that the use of formal techniques enables to successfully detect control program and supervision interface design errors.Show less >
Show more >The Anaxagore Project provides a component-based design ow for reconfigurable socio-technical systems. Each component integrates a control program and a supervision interface and it has been validated by empirical testing. The purpose of this paper is the use of formal methods for the verification of the whole component control-command chain. Different component features (the control program, the supervision interface, the physical device) and the human tasks are modeled using timed automata. These timed automata are then checked by model checking (UPPAAL) with a set of safety and usability properties written in CTL. Our approach is presented through an industrial case study: the supervised control of a 2-way motorized valve. The results show that the use of formal techniques enables to successfully detect control program and supervision interface design errors.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
Collections :
Source :