Towards the analysis of real-time systems: the UML/PNO approach

CONTRIBUTION A LA SPÉCIFICATION DES SYSTÈMES TEMPS RÉELS : L'APPROCHE UML/PNO

Jérôme Delatour (1)

1 LAAS - Laboratoire d'analyse et d'architecture des systèmes

This work focuses on the UML/PNO (Unified Modelling Language with Petri Net Objects) approach for the specification of real-time systems. It enhances the UML dynamic diagrams with the Petri Nets (PN) formal language. The concept of real-time components, called "Compound Object", has been developed as an extension of the UML sub-systems. The aim is to improve the system modelling and structuring. The behaviour of a Compound Object is described by means of time PN. The timing intervals are assigned to PN places and transitions. Thus, formal verification of timing constraints can be done. The validation approach relies upon on the semi-automatic translation of the UML dynamic diagrams into Petri Nets. During such a derivation, some UML diagrams inconsistencies are automatically detected. Then, existing PN tools can be used for simulation and performance analysis. The verification process uses a model-checking analysis based on linear state class graph. When a non-respected timing constraint occurs, a theorem proving approach based on linear logic is used in order to capture the causality relationships. A part of the UML/PNO approach has been integrated in a CASE Tool as an "ArgoPNO" module. It is now available in the ArgoUML environment.

Ce travail présente l'approche UML/PNO (Unified Modelling Language with Petri Net Objects) pour la spécification de systèmes temps réel. La méthode propose d'enrichir la description semi-formelle UML du système par une modélisation formelle basée sur les réseaux de Petri. Les concepts UML de sous-système et d'interface ont été étendus afin d'améliorer la description de la vue système en termes de tructuration, gestion de projet et organisation de la modélisation. L'objectif est également d'adapter la méthode de modélisation système à une approche " orientée composant " pour le temps réel. Le concept " d'objet composé " permet d'intégrer des spécificités temps réel au sein du composant (protocole de communication, contrainte temporelle, effet observable). Le comportement des objets est spécifié à l'aide des réseaux de Petri à places et transitions stochastiques temporelles afin de permettre la validation et la vérification du système en cours de spécification. L'approche de validation propose des traductions semi-automatiques des diagrammes UML en réseaux de Petri. Les techniques classiques de simulation et d'évaluation de performances peuvent alors être appliquées. Ces traductions présentent l'avantage de rassembler, sur un même modèle à réseau de Petri, tous les aspects dynamiques du composant apparaissant dans différents diagrammes UML et de vérifier ainsi la cohérence de son comportement et de son utilisation. La vérification utilise les techniques d'analyse formelle, basées sur l'utilisation conjointe du graphe de classes et de la logique linéaire. Une approche de vérification quantitative des contraintes temporelles est proposée au niveau de l'analyse des besoins et des exigences du système. Une partie de ce travail a été concrétisée par l'intégration d'un module (ArgoPNO) dans l'atelier de génie logiciel ArgoUML. A ce jour, une première automatisation de la démarche de vérification des contraintes temporelles est opérationnelle sur cet outil.

Mots clés: real-time; Petri nets; timing constraints; requirement analysis

Mots clés: UML; temps réel; Réseaux de Petri; contraintes temporelles; analyse des besoins; spécification; validation; vérification

Domaines: Génie logiciel [cs.SE]; Théorie et langage formel [cs.FL]; Systèmes embarqués

Jérôme Delatour. CONTRIBUTION A LA SPÉCIFICATION DES SYSTÈMES TEMPS RÉELS : L'APPROCHE UML/PNO. Génie logiciel [cs.SE]. Université Paul Sabatier - Toulouse III, 2003. Français. ⟨NNT : ⟩. ⟨tel-01044988⟩