Transcription of M-UML specifications into the Maude system

Résumé

First, multi-agent systems form an interesting type of company modeling and, as such, have very broad fields of application. Therefore, the technology field of "mobile agents" represents a new and important concept in artificial intelligence and software engineering. Despite the interest in this technology, most approaches at present do not allow a sufficient and complete design of mobile agents. On the other hand, the Maude system is a specification, object-oriented programming and proof environment based on rewriting logic which is a unifying semantic framework of several concurrency models. In addition, the Maude system also has a battery of tools allowing the simulation and the analysis of accessibility by the LTL (Linear Temporal Logic) Model-Checker enabling the verification and the prototyping of the properties of the specifications. Finally, the UML graphical method and its extensions make it possible to represent systems synthetically and intuitively, multi-agent systems. However, they are not equipped with tools for verification. In this thesis, we address an approach for the transcription of M-UML diagrams in the Maude system. We applied our proposed three-stage approach to the statechart diagram, one of the most important diagrams in M-UML. The technique involves systematically deriving a formal Maude description from this type of diagram analysis, and we obtained very satisfactory results. The proposed transcription makes it possible to obtain an algebraic specification expressed with the rewriting logic. The latter will be used for the verification of properties of mobile agent-based systems.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 2

Téléchargements : 0