Mapping Mobile Statechart Diagrams to the π-Calculus using Graph Transformation: An Approach for Modeling, Simulation and Verification of Mobile Agent-based Software Systems

Mapping Mobile Statechart Diagrams to the π-Calculus using Graph Transformation: An Approach for Modeling, Simulation and Verification of Mobile Agent-based Software Systems

Aissam Belghiat (University Constantine 2 Abdelhamid Mehri, Constantine, Algeria) and Allaoua Chaoui (MISC Laboratory, Department of Computer Science and its Applications, University Constantine 2 Abdelhamid Mehri, Constantine, Algeria)
Copyright: © 2016 |Pages: 20
DOI: 10.4018/IJIIT.2016100101
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Mobile UML (M-UML) has been proposed as an extension of UML to model mobile agent-based software systems. As UML, M-UML suffers from lack of formal semantics due to its semi-formal nature which penalize the verification of correct behavior of the modeled systems. This paper provides a graphical yet formal approach for the modeling, simulation and verification of mobile statechart diagrams using graph transformations in the AToM3 tool. The authors have firstly proposed meta-models for mobile statechart diagram and flowgraph. Then, a twofold graph grammar is developed for the automatic mapping of mo-bile statechart diagrams into flowgraphs and in the same time generates the cor-responding p-calculus specification. This graph grammar enables either execu-tion through simulation by flowgraphs or verification through model checking, using existing tools (e.g. the Mobility Workbench, MWB). An illustrative example of the authors' approach is provided.
Article Preview

Introduction

Modeling and verification of mobile agent-based software systems is a difficult task. This is due to different constraints (mobility, security... etc.) which must be taken into account in these systems to build correct software (Hamidi & Mohammadi, 2008). Multiple attempts for providing a full expressive language for these systems are done in the literature such as Mobile UML (M-UML) (Saleh & El-Morr, 2004). M-UML is an extension of UML (OMG, 2015) to model mobile agent-based applications by covering the mobility feature that represents the novel concept inherent to such systems. It provides multiple views and diagrams including the mobile statechart diagram. This latter can be used easily to specify the lifecycle of different agents, but the problem of formal semantics missing from this language prohibits any attempts to apply rigorous automated verification or to execute these models.

Formal methods have been used largely to deal with such problems (Bouzahzah & Maamri, 2015; Kouah et al., 2016; Lin, 2007). They are adopted as target semantics formalisms. In our case, we need a formalism that is capable to model the mobility feature. Thus, we have chosen the π-calculus (Milner, 1999) which is a process algebra for modeling mobile and concurrent systems. It has a rich theory and tools and considered as the most adapted formalism for mobile agent systems. A difficulty with the π-calculus is its rigorous formal nature that has made it hard to be used for a wider audience. Therefore, providing a π-calculus based approach as in our case might be insufficient for stakeholders, although the advantages offered by the approach. The use of a graphical representation for this formalism must significantly facilitate its interpretation. So, a more promising way is to add a pseudo-simulator (without expensive costs) that explains graphically the execution of mobile statechart diagrams in the π-calculus on real time. This will give an easy comprehension of the dynamic evolution of the modeled systems. We have chosen the flowgraphs (Milner, 1979) for this purpose. By this way, we could obtain a framework for modeling, simulating and verifying mobile statechart diagrams.

To implement the ideas evoked above, we have used the AToM3 tool (AToM3, 2002) (De Lara & Vangheluwe, 2002b) to build our framework. Hence, we have firstly proposed two meta-models for mobile statecharts and flowgraphs to allow their visual modeling in the AToM3 tool. Then, we have developed a twofold graph grammar which simulates the execution of mobile statechart diagrams using flowgraphs and at the same time derives their corresponding π-calculus code. The generated specifications are then used to verify systems using π-calculus analytical tools such as the MWB tool (Victor & Moller, 1994) used here.

The rest of the paper is organized as follows. In Section 2, we present a background concerning M-UML, π-calculus and AToM3. In Section 3, we present the proposed approach to build the framework. In Section 4, an example is presented. In Section 5, some related works are invoked. Section 6 concludes the paper and gives some perspectives.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 14: 4 Issues (2018): 1 Released, 3 Forthcoming
Volume 13: 4 Issues (2017)
Volume 12: 4 Issues (2016)
Volume 11: 4 Issues (2015)
Volume 10: 4 Issues (2014)
Volume 9: 4 Issues (2013)
Volume 8: 4 Issues (2012)
Volume 7: 4 Issues (2011)
Volume 6: 4 Issues (2010)
Volume 5: 4 Issues (2009)
Volume 4: 4 Issues (2008)
Volume 3: 4 Issues (2007)
Volume 2: 4 Issues (2006)
Volume 1: 4 Issues (2005)
View Complete Journal Contents Listing