Sage Journals: Discover world-class research

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 $\pi$ -calculus specifications is proposed. Finally, the derived $\pi$ -claculus specifications are verified and analysed using $\pi$ -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 $\pi$ -calculus tools).

Keywords

Mobile UML π-calculus modelling verification graph transformation AToM3

Get full access to this article

View all access options for this article.

References

AToM

{}^{3}

home page, (online) available at: http://atom3.cs.mcgill.ca/.

Bahri

M.R.

Hettab

Chaoui

and Kerkouche

, Transforming Mobile UML Statecharts Models to Nested Nets Models using Graph Grammars: An Approach for Modeling and Analysis of Mobile Agent-Based Software Systems, in: SEEFM 2009, IEEE Computer Society, Washington, 2009, pp. 33–39.

Belghiat

Chaoui

Maouche

and Beldjehem

, Formalization of Mobile UML Statechart Diagrams using the

\pi

-calculus: An Approach for Modeling and Analysis, in: Dregvaite

and Damasevicius

(Eds.): ICIST 2014, CCIS 465, pp. 236–247. Springer.

Belghiat

et al., Mobile agent-based software systems modeling approaches: A comparative study, CIT. Journal of Computing and Information Technology 24(2) (2016), 149–163.

Belghiat

and Chaoui

, Mapping mobile statechart diagrams to the π-calculus using graph transformation: An approach for modeling, simulation and verification of mobile agent-based software systems, International Journal of Intelligent Information Technologies (IJIIT) 12(4) (2016).

Belghiat

Chaoui

and Beldjehem

, Capturing and Verifying Dynamic Program Behavior Using UML Communication Diagrams and

\pi

-Calculus, in: IEEE International Conference on Information Reuse and Integration, 2015, USA.

Belghiat

and Chaoui

, A

\pi

-calculus-based approach for the verification of UML2 sequence diagrams, in: ICSOFT, the 10th International Joint Conference on Software Technologies, 2015, France.

Belghiat

Chaoui

and Beldjehem

, Capturing and Verifying Dynamic Systems Behavior Using UML and

\pi

-Calculus, in: Theoretical Information Reuse and Integration, Springer, 2016, pp. 59-84.

Bezerra

J.M.

and Hirata

C.M.

, A Polyadic

\pi

-Calculus Approach for the Formal Specification of UML-RT, Advances in Software Engineering, Volume 2009, Article ID 656810, 26 pages, doi: 10.1155/2009/6568102009.

10.

Briais

, The ABC’s User Guide, May 2005.

11.

Chama

Elmansouri

and Chaoui

, Model checking and code generation for UML diagrams using graph transformation, International Journal of Software En-gineering & Applications (IJSEA) 3(6) (November 2012).

12.

DAM

, Model checking mobile processes, in: International Conference on Concurrency Theory, Springer, Berlin, Heidelberg, 1993, pp. 22–36.

13.

Ferrari

G.L.

Gnesi

Montanari

and Pistore

, A model-checking verification environment for mobile processes, ACM Transactions on Software Engineering and Methodology (TOSEM) 12(4) (2003), 440–473.

14.

Frendrup

and Jensen

J.N.

, Checking for Open Bisimilarity in the

\pi

-Calculus, Febuary 2001.

15.

Guerra

and deLara

, A Framework for the Verification of UML Models, Examples using Petri Nets, in: JISBD’03. Alicante.

16.

Guerrouf

Chaoui

and Aldahoud

, A graph transformation approach of mobile activity diagram to nested Petri nets, International Journal of Computer Aided Engineering and Technology 5(1) (2013), 44–57.

17.

Kerkouche

Chaoui

Bourennane

and Labbanic

, A UML and colored petri nets integrated modeling and analysis approach using graph trans-formation, Journal of Object Technology 9(4) (2010), 25–43.

18.

Lam

V.S.W.

, On π-calculus semantics as a formal basis for UML activity diagrams, International Journal of Software Engineering and Knowledge Engineering 18(4) (2008), 541–567.

19.

Lam

V.S.W.

and Padget

, Formalization of UML Statechart Diagrams in the

\pi

-Calculus, in: Proceedings of Software Engineering Conference, Australian, IEEE 2001.

20.

Milner

, Communicating and Mobile Systems: The

\pi

-calculus, Cambridge University Press, 1999.

21.

OMG: Unified Modeling Language (UML), Superstructure, v2.5, http://www.omg.org/, 2017.

22.

Outtagarts

, Mobile agent-based applications: A survey, International Journal of Computer Science and Network Security 9(11) (November 2009).

23.

Pokozy

and Priami

, Toward extracting π-calculus from UML sequence and state diagrams, Electronic Notes in Theoretical Computer Science 101 (2004), 51–72.

24.

Rozenberg

, Handbook of Graph Grammars and Computing by Graph Transfor-mation, World Scientific, 1999.

25.

Saleh

and El-Morr

, M-UML: An extension to UML for the modeling of mobile agent-based software systems, Journal of Information and Software Technology 46 (2004), 219–227.

26.

Vanghluwe

deLara

and Mosterman

, An introduction to Multi-paradigm Modelling and Simulation. Proc. AIS2002. 2002, pp. 9–20. SCS International.

27.

Victor

and Moller

, The Mobility Workbench – A Tool for the

\pi

-calculus, in: Dill

, (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg 1994.

28.

Yang

and Zhang

S.S.

, Using

\pi

-calculus to formalize UML activity diagrams, in: 10th Int. Conf. and Workshop on the Engineering of Computer-based Systems, IEEE Computer Society, 2004, pp. 47–54.

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

Abstract

Keywords

Get full access to this article

References