A. Belghiat and A. Chaoui. 2019. A multi-paradigm approach to model and verify mobile agent software systems. Multiagent and Grid Systems, 14, 4 (January 2019), IOS Press, 337-356. DOI: https://doi.org/10.3233/MGS-180295.

Belghiat, A. & Chaoui, A. (2019, January). A multi-paradigm approach to model and verify mobile agent software systems. Multiagent and Grid Systems, 14(4), IOS Press, 337-356. DOI: https://doi.org/10.3233/MGS-180295

A. Belghiat and A. Chaoui, "A multi-paradigm approach to model and verify mobile agent software systems". Multiagent and Grid Systems, vol. 14, no. 4, IOS Press, pp. 337-356, January, 2019. DOI: https://doi.org/10.3233/MGS-180295.

@article{misc-lab-222,
author = {Belghiat, Aissam and Chaoui, Allaoua},
title = {A multi-paradigm approach to model and verify mobile agent software systems},
journal = {Multiagent and Grid Systems},
volume = {14},
number = {4},
issn = {1574-1702},
pages = {337--356},
publisher = {IOS Press},
year = {2019},
month = {January},
doi = {10.3233/MGS-180295},
url = {https://content.iospress.com/articles/multiagent-and-grid-systems/mgs180295},
keywords = {Mobile UML, π-calculus, modelling, verification, graph transformation, AToM3}
}

TI  - A multi-paradigm approach to model and verify mobile agent software systems
AU  - A. Belghiat
AU  - A. Chaoui
PY  - 2019
SN  - 1574-1702
JO  - Multiagent and Grid Systems
VL  - 14
IS  - 4
SP  - 337
EP  - 356
PB  - IOS Press
AB  - 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).
KW  - Mobile UML
KW  - π-calculus
KW  - modelling
KW  - verification
KW  - graph transformation
KW  - AToM3
DO  - 10.3233/MGS-180295
UR  - https://content.iospress.com/articles/multiagent-and-grid-systems/mgs180295
ID  - misc-lab-222
ER  -