Affiliations: [a] University of Mohamed Seddik Benyahia-Jijel, Jijel, Algeria | [b] MISC Laboratory, University of Constantine 2 – Abdelhamid Mehri, Constantine, Algeria
Correspondence:
[*]
Corresponding author: Aissam Belghiat, University of Mohamed Seddik Benyahia-Jijel, Jijel, Algeria. E-mail: [email protected].
Abstract: Modelling and verification of complex systems including mobile agent-based software systems are a painful task, because of different constraints such as mobility and security which must be taken into account to build correct software. This is what strongly hindered their evolution in preceding years in comparison to the success enjoyed by object oriented systems. UML has contributed largely in the success of object oriented systems. Mobile UML is a proposed extension to UML for modelling mobile agent-based software systems, and it inherits the problem of no precise formal semantics due to its semi-formal nature. This paper aims to build a semi-formal/formal framework that allows modelling and verification of mobile agent-based applications. First, a mobile agent-based application is modeled using Mobile UML diagrams. Then, an automatic translation of these diagrams to π-calculus specifications is proposed. Finally, the derived π-claculus specifications are verified and analysed using π-calculus tools. The AToM3 multi-paradigm tool is used to implement the approach. The result is an integrated framework that allows visual modelling (using Mobile UML diagrams) and formal verification of the behaviour of mobile agent-based applications (using π-calculus tools).
Keywords: Mobile UML, π-calculus, modelling, verification, graph transformation, AToM3
