EMI : Un Interpréteur de Modèles Embarqué pour l’Exécution et la Vérification de Modèles UML

Pour faire face a la complexite croissante des systemes embarques, les activites de verification et de validation, et notamment le model-checking, sont de plus en plus sollicites. Les model-checkers permettent de verifier des proprietes par rapport au modele formel fourni en entree mais deux problemes subsistent generalement. D’une part, les outils de model-checking n’apportent pas l’assurance que les proprietes sont aussi verifiees sur le code executable du systeme. D’autre part, le modele formel utilise par les modelcheckers est souvent le resultat d’une transformation de modele dont l’exactitude n’est pas prouvee. Pour y remedier, cet article presente EMI, un interpreteur de modeles UML visant l’execution et la verification de systemes embarques a l’aide d’une seule implementation de la semantique du langage. En connectant cet outil au model-checker OBP2, diverses activites de verification peuvent ainsi etre menees sur des modeles semi-formels en UML.