Formalisation des spécificationsumlmarte par les réseaux de Petri temporellement temporisés en vue de lavérification formelle des systèmes temps-réel embarqués

Voir Plus Voir Moins

Afficher le Résumé

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 umlL 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-checkertels 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).184044-46/22