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 AToM 3 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).

Search results

A multi-paradigm approach to model and verify mobile agent software systems

Towards Domain-specific Model Editors with Automatic Model Completion