Mesli-Kesraoui, S., Kesraoui, D., Berruet, P. et Oquendo, F. (2023) Verification of Control-Command Programs: Counterexample Explanation by Simulation. Dans CIGI Qualita MOSIM 2023, Trois-Rivières, Québec, Canada DOI 10.60662/2dtf-f320.
Prévisualisation |
Texte
CIGI_QUALITA_MOSIM_2023_paper_988.pdf Télécharger (872kB) | Prévisualisation |
Résumé
Afin de faciliter la compréhension et l’interprétation des contre-exemples, retournés par les Model-Checkers, cet article présente une approche, basée sur l’IDM pour la visualisation et la simulation automatique des contre-exemples Uppaal (traces) directement sur les programmes de contrôle-commande. En effet, les traces Uppaal sont transformées automatiquement en des traces génériques, indépendantes de plateformes. Un métamodèle modélisant ces traces génériques, résultant de l’exécution des programmes de contrôle-commande selon la norme PLCOpen, est également proposé. Les traces génériques sont ensuite transformées en des traces spécifiques, directement simulables par des plateformes de fournisseurs. Notre approche a été validée sur un cas d’étude industriel concret.
In order to facilitate the understanding and the interpretation of the counterexamples returned by ModelCheckers, this paper presents an MDE-based approach for the automatic visualization and simulation of the Uppaal counterexamples (traces) directly on the control-command programs. Indeed, Uppaal traces are automatically transformed into generic (platform-independent) traces. A metamodel modeling the generic traces resulting from the execution of the control-command programs, according to the PLCOpen standard, is also proposed. The generic traces are then transformed into specific traces, which can be directly simulated on vendor-platforms. Our approach has been validated on a concrete industrial case study
Type de document: | Document issu d'une conférence ou d'un atelier (NON SPÉCIFIÉ) |
---|---|
Mots-clés libres: | Simulation de contre-exemple Rétro-Annotation Model checking Programmes de contrôle-commande API Counterexample simulation Back-annotation Model checking Control-command programs PLC |
Date de dépôt: | 15 août 2023 18:52 |
Dernière modification: | 30 août 2023 12:58 |
URI: | https://collection-numerique.uqtr.ca/id/eprint/1999 |
Actions (administrateurs uniquement)
Éditer la notice |