Vérification formelle de la relation de raffinement des diagrammes de séquences d'UML2.X avec la méthode formelle B événementiel

Autor: Dhaou, Fatma
Přispěvatelé: dhaou, fatma
Jazyk: francouzština
Rok vydání: 2018
Předmět:
Popis: The main research topic of this thesis revolves around the use of sequence diagrams for the modeling of behaviours of distributed systems deemed as a complex problem. We especially address the application of refinement process for UML2.X sequence diagrams (SD) that seems to be a good way for handling this complexity by building behaviours incrementally.The verification of refined SD against each others is a necessity, this requires a formal semantics.The first challenge consists in finding a suitable semantics that permits the computation of all possible valid behaviours for this kind of systems.The most state-of-the art approaches are based on standard semantics, which proposes rules that didn't permit to obtain all possible valid behaviours for distributed systems.To tackle this challenge, we choose an existing semantics which is suitable for distributed systems, however it is proposed for UML1.X SD, therefore we extend its rules to deal with UML2.X SD that are equipped with a high level structures.Our operational semantics is a solid starting point for the formalization of refinement relation, since it is concretely given as a labeled transition system (LTS), and knowing that the refinement relation are well-defined on LTS. Which helps us to the formalization of refinement relation on UML2.X SD.Consequently, the second line of research focuses on this goal. The rules that govern a correct refinement between SD pairs are clearly defined and a refinement relation between sequence diagrams is formulated.The last line of research is the implementation of our approach with the formal method Event-B. It provides powerful tools for the verification by theorem prover and model checking. A generic model of verification refinement relation is proposed.
Ce travail s'inscrit dans la thématique de vérification formelle des diagrammes de séquence (DS) d'UML2.X qui sont construits de façon incrémentale, correspondant au processus de raffinement, et qui modélisent les comportements des systèmes distribués. La vérification de la correction des DS raffinés nécessite une sémantique formelle qui supporte le processus de raffinement.Une étape préliminaire qui est la première contribution de notre travail, nous avons équiper les DS avec une sémantique adéquate aux systèmes distribués ; une sémantique dont les relations tiennent compte de l'indépendance des composants participant à l'interaction et elles permettent de calculer toutes les traces possibles valides. Partant une sémantique existante, qui est destinée uniquement aux DS basiques, nous l'avons étendu pour qu'elle supporte les DS avec fragments combinés. Nous avons défini une sémantique opérationnelle basée sur cette sémantique d'ordre partiel. La sémantique opérationnelle nous a procuré l'avantage d'exprimer et de formaliser la relation de raffinement en exploitant les relations de raffinement, déjà existantes, qui sont exprimées sur les systèmes de transitions étiquetées (\textit{labelled transition system} (LTS)), étant donnée qu'une sémantique opérationnelle décrit un LTS.Le deuxième volet de notre travail consiste à appliquer le processus de raffinement sur les diagrammes de séquence d'UML2.X ; deux aspects majeurs doivent être considérés dans le raffinement des DS qui sont sa structure et sa sémantique (ses traces). Les travaux de l'état de l'art considèrent un seul aspect à la fois en imposant des hypothèses strictes pour l'autre aspect ce qui peut être contraignant pour l'ingénieur. En raffinant un DS, de nouveaux éléments (événements, lignes de vie, etc...) peuvent être ajoutés dans le DS, pour vérifier le raffinement, ces éléments vont être cachés, pour obtenir deux modèles possédant le même alphabet, sans faire aucune vérification au préalable de la correspondance entre les éléments abstraits et raffinés des deux DS considérés. En procédant ainsi, dans le cas où des erreurs de modélisations seront commises, elles ne peuvent pas être détectées. D'autant plus que la non divergence de nouveaux événements ne peut pas être vérifier.Pour surmonter ces insuffisances, nous considérons un raffinement des DS qui traite les deux aspects structurel et sémantique. Nous énonçons des règles claires qui régissent un raffinement correct. La relation de raffinement formalisée est basée sur une correspondance explicite entre les éléments abstraits et raffinés des deux DS considérés ce qui permet de détecter les erreurs de spécification et de les corriger.Puisque semi formé, le langage UML ne permet pas de vérifier des propriétés des modèles UML. Le couplage d'une méthode formelle qui supporte le raffinement des données et des traces est une approche privilégiée procurant une rigueur de l'approche proposée.Dans cet objectif, notre deuxième contribution consiste à l'implémentation de notre approche avec la méthode B événementielle qui répond aux critères recherchées et qui est en plus dotée d'outils puissants de vérification par la preuve et par l'explorateur de modèle model-checking. Des propriétés intrinsèques au DS sont vérifiées ainsi que des propriétés de sûreté, de vivacité et de non divergence sont aussi exprimées et vérifiées. Des expérimentations sur des études de cas ont été menées.
Databáze: OpenAIRE
Externí odkaz: