Verification of Control-Command Programs: Counterexample Explanation by Simulation

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