Formalisation Des Spécifications Uml Marte Par Les Réseaux De Petri Temporellement Temporisés En Vue De La Vérification Formelle Des Systèmes Temps-réel Embarqués

Résumé: Les systèmes temps-réel embarqués (STRE) sont souvent complexes et critiques, et nécessitent un développement rigoureux pour affirmer leur correction fonctionnelle sous des contraintes temporelles. Le profil UML MARTE (Modeling and Analysis of Real Time Embedded systems) est imposé comme un standard spécifié par l’OMG pour la modélisation et l’analyse des systèmes temps-réel embarqués. Il offre un Framework général de modélisation pour concevoir et analyser les STRE. Cependant, les spécifications en modèles UML MARTE manquent de fondements formels requis pour accomplir une vérification complète de ces modèles. De ce fait, les modèles UML MARTE ne peuvent pas être exploités à des fins de vérification et validation des systèmes. Une combinaison des modèles UML MARTE et des méthodes formelles est une alternative pour surmonter un tel problème. Dans ce contexte, la vérification formelle basée modèle (model-checking) constitue un outil important du fait qu’elle est dotée de procédure permettant la vérification automatique et exhaustive des propriétés attendues du système en étude. Malgré son importance, la vérification basée modèle se heurte au problème de l’explosion combinatoire de l’espace d’états, en particulier si le nombre des horloges est important. Le travail de cette thèse s’inscrit dans le cade de la spécification et la vérification formelle des systèmes temps-réel embarqués. Il consiste à tirer profit des avantages offerts par les modèles formels temporellement temporisés et basés sur les sémantiques du vrai parallélisme. Ainsi, nous présentons dans un premier temps, une approche orientée modèle pour spécifier et vérifier formellement les systèmes temps-réel embarqués décrits par les modèles UML MARTE. Par ailleurs, nous formalisons la sémantique des diagrammes de séquence UML2 annotés par des contraintes temporelles en utilisant le profil MARTE. Ainsi, nous proposons une méthode opérationnelle de translation de ces diagrammes vers les réseaux de Petri temporellement temporisés (DTPNs). Les règles graphiques et formelles de la translation (MARTESDtoDTPN) sont développées et appliquées sur des exemples illustratifs. La vérification formelle exploite les structures sémantiques associées aux spécifications décrites en DTPN, à savoir les automates temporisés avec durées actions (daTAs). En effet, l’espace d’états d’un daTA est exprimé par un graphe de régions ou par un graphe de zones basé sur la maximalité, et la vérification peut se faire par des outils model-checker tels que UPPAAL ou KRONOS. Cette contribution est validée sur un cas d’étude d’un système temps-réel embarqué, en l’occurrence le système de contrôle d’ascenseurs (SCA).

Publié dans la revue: