Formal and Joint Verification of Control ...
Type de document :
Communication dans un congrès avec actes
Titre :
Formal and Joint Verification of Control Programs and Supervision Interfaces for Socio-technical Systems Components
Auteur(s) :
Mesli, Soraya [Auteur]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
ArchWare
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]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192) [Lab-STICC]
ArchWare
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]
Titre de la manifestation scientifique :
Proceedings of the 13th IFAC Symposium on Analysis, Design, and Evaluation of Human-Machine Systems (HMS 2016)
Ville :
Kyoto
Pays :
Japon
Date de début de la manifestation scientifique :
2016-08-30
Titre de l’ouvrage :
Journal IFAC PapersOnLine (Elsevier)
Éditeur :
IFAC
Mot(s)-clé(s) en anglais :
Formal Verification
Control-Command
HMI
Model Checking
CTL
Control-Command
HMI
Model Checking
CTL
Discipline(s) HAL :
Informatique [cs]/Génie logiciel [cs.SE]
Sciences de l'ingénieur [physics]
Sciences de l'ingénieur [physics]
Résumé en anglais : [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. ...
Lire la suite >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.Lire moins >
Lire la suite >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.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :