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

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 AToM³ tool (AToM³, 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 AToM³ 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 AToM³. 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.