UML et Model-Checking pour la Modélisation et la Vérification des Systèmes Embarqués

Abstract

Ce travail présente une approche formelle de modélisation et de vérification des systèmes embarqués. L’approche repose sur une modélisation du comportement temporel du système et une génération automatique de code. Le concept clé est l'utilisation combinée d'un ensemble de diagrammes comportementaux d’UML étendu par des annotations temporelles (diagrammes Statechart temps réel et de collaboration temps réel) pour la modélisation du système et le langage Maude pour la vérification. Tout d'abord, un outil de modélisation UML est développé, ensuite, une grammaire de graphes est exécutée pour générer automatiquement des spécifications en Maude équivalentes. L'approche repose sur la génération de code, donc il est possible d'utiliser un outil de vérification de modèles (Model-cheking) pour vérifier certaines propriétés temporelles représentées dans la logique temporelle temps réel (MITL).