Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics

Vlad Rusu 1 Laure Gonnord 2, 1 Benoît Combemale 3
1 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
3 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Résumé : Le besoin en définitions rigoureuses de langages de modélisation métiers (LMM) croît avec la complexité du développement logiciel. L'ingénierie dirigée par les modèles (IDM), permet à des utilisateurs de définir la syntaxe de nouveaux langages à l'aide de metamodèles. Quelques approches proposent également des façons de définir la sémantique opérationnelle de ces langages. Ces approches permettent, en principe, l'exécution des programmes (modèles) et leur analyse formelle. Cependant, la plupart du temps, les analyses sont réalisées à l'aide de transformations de ces modèles vers d'autres langages, pour être exécutés (langages généralistes, type C par exemple) ou vérifiés (langages d'entrées de model checkers, de simulateurs, ...). En conséquence, ces résultats (un log de crash de programme, une exécution contre exemple provenant de la vérification d'une propriété par un model-checker, par exemple) peuvent ne pas être directement compréhensibles par les utilisateurs d'un LMM. Dans ce rapport, nous proposons une méthode formelle et opérationnelle pour exprimer ces exécutions en terme de syntaxe et sémantique du LMM initial.
Type de document :
Rapport
[Research Report] RR-7423, INRIA. 2010
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00526561
Contributeur : Laure Gonnord <>
Soumis le : vendredi 15 octobre 2010 - 08:54:56
Dernière modification le : mercredi 16 mai 2018 - 11:23:06
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 17:20:16

Fichier

RR-7423.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00526561, version 1

Citation

Vlad Rusu, Laure Gonnord, Benoît Combemale. Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics. [Research Report] RR-7423, INRIA. 2010. 〈inria-00526561〉

Partager

Métriques

Consultations de la notice

393

Téléchargements de fichiers

199