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

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

1. Introduction

Mobile agent-based software systems have shown multiple advantages in a wide range of domains such as: network management, electronic commerce, energy efficiency, grid computing, distributed data mining, wireless multimedia sensors, and multimedia [22]. In fact, the mobile agent paradigm provides multiple benefits, such as its heterogeneous nature, it operates asynchronously, it adapts dynamically and reacts autonomously to changes, which could overcame and solve several problems in different fields. Mobility is the novel concept of the paradigm; it is the agent capability of moving from a host to another where it continues its execution in order to achieve a task. The modelling and verification of the behaviour of such systems is still a tough task, because mobility produces complicated dynamic reconfiguration of the system in question during its execution.

Having an appropriate approach, that used to model and verify such systems during the design phase, should enhance building correct software which respond to the user’s requirements. Multiple attempts for developing a rich expressive language for these systems are performed in the literature, such as Mobile UML (M-UML) [25]. M-UML is an extension of UML [21] that deals with modelling mobile agent-based applications, by covering the mobility aspects which is considered as the main concept inherent to such systems. M-UML has no formal semantics, so it cannot support formal analysis or verification of their models. On the other side, the $\pi$ -calculus is a process theory proposed by Milner [20] for formal specification of mobile and concurrent systems. It is characterized by its rich theory and tools, and regarded as the most adopted formalism, especially for mobile agent systems.

This work is part of a project that aims to provide a complete practical integrated approach, which can be used to specify and verify automatically mobile agent-based software systems. Our previous works include a state of the art of different methods and tools that have been developed for modelling mobile agent-based software systems [4]. This last led us to propose a partial contribution that consists on using graph transformation for mapping mobile statechart diagrams to $\pi$ -calculus [3, 5], that is supposed to model, simulate and verify such systems. There was also an attempt to give formal semantics to interaction diagrams using also $\pi$ -Calculus [6, 7, 8].

In contrast to these works, the idea of multi-paradigm modelling [26] is adopted in the present paper for modelling and verifying mobile agent applications. Actually, two formalisms are used; M-UML and the $\pi$ -calculus. In M-UML, three diagrams have been selected (mobile class diagram, mobile statechart diagram and mobile collaboration diagram), which are used to model different views of a mobile agent-based software system, and can be considered as the main and essential diagrams to model such systems. The $\pi$ -calculus is adopted as the target verification formalism for such diagrams.

This work plans to generate a very rich description of behaviour of every system modelled in our framework. To reach this goal, and in order to maintain coherence and consistency between different diagrams, we have chosen a driving type of diagrams (in our case, the mobile statechart diagram) and we add necessary information about the system from the other types of diagrams (in our case, the mobile class diagram and the mobile collaboration diagram). A mobile statechart-driven approach provides a detailed description compared to the mobile collaboration-driven approach, actually, the behaviour of each agent is specified in satisfactory details using the first approach.

Regarding other diagrams, the class diagram brings interesting information about the relation between agents which belongs to its classes, and also more details about their behaviour in its methods. The collaboration diagram brings interesting information about communication between the agents (statecharts). The details are given in Section 4.3.1.

To implement the framework, the AToM ${}^{3}$ tool [1] which is an open, multi-paradigm formal framework is used to automate the approach. Therefore, we have proposed a meta-model for three diagrams of mobile UML (mobile class diagram, mobile statechart diagram and mobile collaboration diagram). Then, we have used the AToM ${}^{3}$ capabilities to generate an integrated environment which expected to support the visual modelling of these diagrams. Afterwards, we have proposed and developed a graph grammar which translates, firstly, mobile statechart diagrams to the $\pi$ -calculus. This graph grammar implements the formal mapping proposed in [3]. In addition, during its execution, it takes necessary additional information from the other types of diagrams (i.e. mobile class diagram and mobile collaboration diagram). The derived $\pi$ -calculus specifications are then used to analyze and check mobile systems using automatic $\pi$ -calculus analytical tools, such as: Mobility Workbench (MWB) [27], Bisimulation Checker (ABC) [10], Open Bisimulation Checker (OBC) [14] and HDAutomata Laboratory (HAL) [13]. In our work the MWB tool [27] is used because it provides at once different verification techniques we are looking for, such as model checking, equivalence checking and simulation.

The rest of the paper is organized as follows. Section 2 exposes multiple related works. Section 3 presents a background of M-UML, $\pi$ -calculus, graph transformation in AToM ${}^{3}$ tool and analysis using MWB. Section 4 explains the proposed approach to build the framework. Section 5 illustrates the framework through an example. Section 6 discusses the work done. Section 7 concludes the paper and gives some perspectives.

2. Literature review

The literature is filled with the approaches which try to give formal semantics to UML and its extensions using formal methods in the purpose of enabling automatic verification. In fact, we have already made in [4] a systematic discussion on the literature about techniques and approaches of modelling and verification of mobile agent-based software systems. A taxonomy is given and the major issues of the research area are identified such as mobility modelling. The authors classified existing proposals in three large categories: UML-based Approaches, Formal Approaches and Hybrid Approaches. A comparison framework was developed also. The study concludes by considering the category of hybrid approaches as the most promising techniques, because adopting the combination of visual approaches and formal approaches provides great benefits including intuitive manipulation and analysis enabling. The interested reader can refer to [4] for the details of the study. We recall here some contributions, which belong to the category of hybrid approach and which are very close to our work either in using $\pi$ -calculus as semantic domain or the multi-paradigm tool AToM ${}^{3}$ .

Ragarding the use of $\pi$ -calculus for modelling UML, the authors in [9] have proposed a $\pi$ -calculus based approach to specify UML-RT; a UML profile that allows modelling runtime systems. The authors in [19] have proposed a formalization of statechart diagrams using the $\pi$ -calculus by a bottom-up approach. In [28, 18], a formalization of a subset of UML activity diagram is developed by choosing $\pi$ -calculus as the semantic domain, the second work covers more notational elements and provides a full framework. In [23] an automatic translation of UML specifications made up of sequence and state diagrams into $\pi$ -calculus processes is provided.

Ragarding the use of the Multi-paradigm tool AToM ${}^{3}$ , there was several works. In [15], a framework has been developed for the verification of UML models using Petri Nets. They proposed meta-models for an UML design (composed of Class, Statecharts and Sequence diagrams) in addition to a Petri Nets meta-model. Then, they used graph grammars to translate the former to the later which allows their verification by model checking. In [17], the authors have used an UML design composed of statechart and collaboration diagrams to propose an integrated approach for modelling and analysis of such models. They have used graph transformation in mapping the diagrams into Colored Petri net models. In [11], the authors have used a subset of UML diagrams to develop a framework for their model checking by transforming them into a rewriting system expressed in the Maude language.

Our work, contrary to all preceding contributions, tackles a subset of mobile UML (i.e. mobile applications), uses three types of diagrams at once and derives $\pi$ -calculus specifications, also it provides an automation of the approach.

The semantics of UML diagrams which include mobility were handled in [2, 16]. The authors in [2] have used meta-modelling and graph grammars to propose an approach for the automatic transformation of mobile UML statechart diagrams to nested nets. The purpose is enabling modelling and analysis of mobile agent-based software systems. The same objective has encouraged the authors in [16] to propose an approach, based on meta-modelling and graph transformation, to transform mobile activity diagrams into nested Petri nets to deal with another modelling view of such systems.

Although the two last contributions are very beneficial and interesting, we had some concerns on the target formalism adopted, i.e. Nested Nets formalism, which does not offer tools to enable automatic analysis and verification, besides its limits in providing explicit modelling of mobility in comparison with the $\pi$ -calculus when addressing such systems, indeed, the $\pi$ -calculus provides a rich rigorous theory and tools. In addition, while the previous attempts are focused only on one diagram, this paper handles other types of diagrams in order to gather more interesting information needed to generate a rich $\pi$ -calculus specification. Indeed, our contribution considers that the system is modelled using multiple mobile statechart diagrams, one mobile class diagram and one mobile collaboration diagram.

3. Preliminaries

3.1 Mobile UML (M-UML)

Mobile UML (M-UML) [25] is an UML extension which is expected to deal with the modelling of mobility requirement in mobile agent-based applications. M-UML covers all aspects of mobility at different views and diagrams of UML. We are concerned in this work with three diagrams among them; the mobile class diagram, the mobile collaboration diagram and the mobile statechart diagram. A description of these diagrams is given here.

A mobile class diagram (see the example in Fig. 4b, its description will be given in Section 5.1) represents the internal static structure of the mobile software system by showing its classes and the relationships among them. In short, this diagram adds the notions of mobile classes (from which mobile agents are created), affected classes (containing behaviour, i.e. methods that are communicating with mobile agents), and remote classes (containing behaviour, i.e. methods that are communicating with remote mobile agents).

A mobile collaboration diagram (see the example in Fig. 5b, its description will be given in Section 5.1) is an interaction diagram that shows the interaction behaviour of agents using a sequence of exchanged messages. In short, this diagram adds notions of local interactions (occurring at the same platform), remote interactions (one or both of the two interacting agents are away from their platform) and self-loop interactions (to represent the mobile agent returning to its original platform).

A mobile statechart diagram (see the example in Fig. 3b, its description will be given in Section 5.1) describes the behaviour of an agent in terms of state change in different platforms. In short, this diagram adds the notions of mobile states (states reachable by the agent far from of its base platform), mobile transitions (transitions between two states which are reachable by the agent while they occur at two different platforms), remote transitions (occur when the agent interacts with another agent remotely to reaches a state), and return transitions (which used to represent the mobile agent returning to its base platform by reaching a state on it).

3.2 $\pi$ -calculus

The $\pi$ -calculus [20] is a formal method developed by Milner.1 It is a process algebra used to specify distributed systems, especially mobile concurrent systems. Two major concepts are used by the $\pi$ -calculus: a process; which is an active communicating entity in the system, and a name; which is anything else, e.g. a communication link, data, etc. The $\pi$ -calculus covers the limitation of others calculus in terms of expression power, by allowing the passage of “channels” among processes. Let $P$ , $Q$ two processes, and $x,y,...,y_{1}$ , …, $y_{n}$ are channels, the abstract syntax of the $\pi$ -calculus is given by the following Backus normal form (BNF):

$P::=$ 0	Nil; which means an empty process
$\|\bar{x}<y>.P$	Output prefix; which means send $y$ along $x$
$\|x(y).P$	Input prefix; receive $y$ along $x$
$\|\tau.P$	Silent prefix; which means an internal action
$\|P+Q$	Non-deterministic choice; which means executing $P$ or $Q$
$\|P\|Q$	Parallel composition; which means executing $P$ and $Q$ in parallel
$\|!P$	Replication; which means replication of the process $P$
$\|(\nu x)P$	Restriction; which means restriction of the name $x$ to only the process $P$
$\|[x=y]P$	Match; which means if $x=y$ then execute $P$
$\|[x\neq y]P$	Mismatch; which means if $x\neq y$ then execute $P$
$\|A(y1,\ldots,yn)$	Process Identifier; which means a process with arguments

Furthermore, the following shortcuts are defined:

$\prod\nolimits_{i\in I}{P_{i}}\mathop{=}\limits^{\textit{def}}{P_{1}\|...\|P_{n}}$	composition of many processes
$\sum\nolimits_{i\in I}{P_{i}}\mathop{=}\limits^{\textit{def}}{P_{1}+...+P_{n}}$	summation of many processes
$\vec{x}_{1}\mathop{=}\limits^{\textit{def}}x_{1},x_{2},...,x_{n}$	series of many channels

The semantics of $\pi$ -calculus is defined by reductions or transitions on the set of processes $P$ of the algebra. In this paper, the focus is on reduction semantics which is enough to describe all interactions. The reductions, denoted by $\to$ , between processes specify the evolution of processes when they execute an atomic calculus. The structural congruence relation $\equiv$ is used by the semantics of reductions.

Table 1 recapitulates the reduction operational semantics of the $\pi$ -calculus [20]. The TAU rule shows that the process on the left of the arrow executes an intera-action (with a non-explicit origin) expressed by $\tau$ and evolves to $P$ . Other capabilities of the component, expressed by $M$ are rendered void. The REACT rule shows that the process on the left of the arrow has two components. Their capabilities are to send $y$ via $x$ on one hand, and to receive a name via $x$ in the other. REACT expresses a reduction arising from an interaction via $x$ between the two componenents, and as effects of this reduction $y$ is passed from the first component to the second and is substituted for the placeholder $z$ in $Q$ . The two prefixes are consumed, so the process on the left evolves to $P|Q_{\{y/z\}}$ . The PAR rule expresses that if the process $P$ has a reduction to $P^{\prime}$ , then the component $P|Q$ itself has a reduction in which the effect is just the effect on $P$ , and it unaffectes the process $Q$ . The RES rule indicates that restriction of a name does not inhibit a reduction. The STRUCT rule says that expressions structurally congruent have the same reductions. If the process $P$ (resp. $Q$ ) is structurally congruent with $P^{\prime}$ (resp. $Q^{\prime}$ ), and the process $P^{\prime}$ has a reduction to $Q^{\prime}$ , then $P$ has a reduction to $Q$ .

3.3 Graph grammars in AToM ${}^{3}$

AToM ${}^{3}$ [1] is a multi-paradigm modelling tool that allows using multiple formalisms at a time. It is considered as a powerful tool for model transformations, and it uses a combination of meta-modelling and graph transformation to realize them. Meta-modelling in AToM ${}^{3}$ is used to specify the abstract syntax and the concrete syntax of any formalism. Graph grammars [24] are implemented in AToM ${}^{3}$ using several compartments. It is composed of three compartments; an initial action, a set of rules and a final action. The initial and final actions are used to provide necessary information before and after the execution of the rules. Each rule has essentially two compartments; a graph on its left hand side (LHS) and a graph on its right hand side (RHS). A host graph is a zone in an input graph, and the rule is evaluated by comparing its LHS with this host graph. If a matching is found, the rule executes, and the RHS of the rule replaces the matching host graph. A condition and an action may be present on the rule. A rewriting system in the graph grammar is used to apply the matching rules iteratively to the host graph until no more rules are applicable. An order is adopted in the rules in this tool using a user-assigned priority.

Table 1
Reduction semantics of the $\pi$ -calculus

TAU: $\tau.P+M\to P$	REACT: $\overline{\bar{x}<y>.P\|x(z).Q\to P\|{\{}y/z{\}}Q}$
PAR: $\frac{P\to P^{\prime}}{P\|Q\to P^{\prime}\|Q}$	RES: $\frac{P\to P^{\prime}}{(\nu x)P\to(\nu x)P^{\prime}}$
STRUCT: $\frac{P\equiv P^{\prime}\quad P^{\prime}\to Q^{\prime}\quad Q^{\prime}\equiv Q% }{P\to Q}$

Taken the example of a sample graph grammar in Fig. 1, to improve general understanding of graph transformation. The graph grammar GG is composed of two rules R1, R2, which are applied on a source graph to generate a target graph. A source graph is composed of linked circles and hixagones. A target graph is composed of parallelograms and trapezes. The rule R1 has a circle node as LHS and a parallelogram node as RHS, its priority is one, so it will be the first rule in execution. The rule R2 has a hixagone node as LHS and a trapeze node as RHS, so it will be the second rule in execution. Conditions before each rule and the actions after will be written in syntax of the transformation engine. Thus, applying GG on each source graph provided composed of circles and hixagones, we will obtain at the end of the execution a target graph composed only of parallelograms and trapezes.

Figure 1.

Graph transformation principle.

3.4 Analysis with mobility workbench (MWB)

The mobility workbench MWB [27] is a tool developed to enable the automation of the analysis of $\pi$ -calculus specifications by letting the computer draws labeled transition systems (LTSs) (as denotation) for $\pi$ -calculus process expressions. It can be used for: Model checking of a subset of mobile UML diagrams using mu-calculus formulas [12], Equivalence checking between different subsets of mobile UML diagrams diagrams, and Interactive simulation of process execution. The approach adopted in the MWB tool to verify the properties is the “on-the-fly” approach.

4. The proposed modeling and verification framework

4.1 The architecture of the framework

In the framework, a combined meta-modelling and graph grammar approach is adopted to build an integrated tool using AToM ${}^{3}$ (see Fig. 2). The approach consists of two essential tasks: Firstly, we need to propose a meta-model for each diagram (steps 1, 2, 3) to generate an AToM ${}^{3}$ integrated environment (step 4) which supports visual modelling of these diagrams (step 5). Secondly, we propose and develop a graph grammar (step 6) which takes the mobile statechart diagrams modelled in the tool, adds necessary information from the others diagrams (the mobile class diagram and the mobile collaboration diagram) and returns us their corresponding $\pi$ -calculus process expressions (step 7) stored in a file on disk and uploaded in the MWB (step 8) to start the verification task.

Figure 2.

The architecture of the developed framework.

4.2 Meta-modelling of M-UML diagrams

Modelling M-UML diagrams needs building an environment that allows their specification. Developing an environment from scratch is a very hard and costly task. Metamodelling was experimented as an effective solution. Thus, we formally specify them by means of meta-modelling. Each meta-model proposed has an abstract syntax and a concrete syntax which facilitate the description of these models. In the next lines, the implementation details of these metamodels which represent a part of the framework are described. The user of the framework (the analyst) should not understand such meta-models, but only specifies his system.

4.2.1 Mobile statechart diagram meta-model

Figure 3a illustrates the proposed meta-model of M-UML statechart diagrams named “EtatTransitionMobileMM” using AToM ${}^{3}$ . The meta-model consists of five classes and eleven transitions. The classes “ETEtatInitial”, “ETEtatFinal”, “ETEtatSimple”, and “ETEtatMobile” to represent respectively initial states, final states, simple states, and mobile states. They inherent from a super-class “ETEtat”. The associations “ETTransitionSF”, “ETTransitionIS”, “ETTransitionADistanceSS”, “ETTransitionSS”, “ETAgentReturnMS”, “ETTransitioMobileSM”, “ETTransitioMobileMS”, “ETTransitioMobileMM”, “ETTransitionADistanceMM”, “ETTransitionMM”, “ETTransitionMF” are used to represent different transitions in a mobile statechart diagram. Figure 3 shows on its right a mobile statechart diagram built using the generated tool.

Figure 3.

Mobile statecharts.

4.2.2 Mobile class diagram meta-model

Figure 4a shows the meta-model “MobileClassDiagramMM” proposed for M-UML class diagrams using AToM ${}^{3}$ . It is composed of two classes and four associations. A class “Package” to represent packages. A class “Class” to represent different types of classes. The associations “Association”, “Generalization”, “AssociationClass”, “Dependency” to represent different relationships in a mobile class diagram. Figure 4 shows on its right an example of a mobile class diagram which is described using the generated tool that is built by the mobile class diagram meta-model.

Figure 4.

Mobile class diagrams.

4.2.3 Mobile collaboration diagram meta-model

Figure 5a shows the meta-model “MobileCollaboration DiagramMM” proposed for M-UML collaboration diagrams using AToM ${}^{3}$ . It is composed of one class and an association. A class “Object” to model different types of agents. An association “Link” to model different types of interactions between agents. Figure 5 shows on its right an example of a mobile collaboration diagram which is described using the generated tool that is built with the defined mobile collaboration diagram meta-model.

Figure 5.

Mobile collaboration diagrams.

4.3 Transformation of M-UML models into the

\pi

-calculus

4.3.1 Semantics rules

Mobile statechart diagrams are already transformed into the $\pi$ -calculus and the formal mapping is defined in detail in [3]. It remains only identifying how they take necessary additional information from the other types of diagrams.

Table 2 recalls the mapping. In fact, the principle concept is that each agent in the diagram is represented by a parameterized process “Si()”, which represents its bahavior in its current state. This process will evolve to another process that represents its next state everytime the agent on the diagram changes its state to another one by performing a transition. Concerning the next state, it could be on the same platform as it could be at another one. The mobility of an agent is modeled by movement of links during the interaction between its corresponding process with a special process, used to represent the platform, named “Platform Scheduler (PS)”. This last is the responsible of enabling the movement of an agent (process) by authorizing it to reach or leave a platform. Each platform is recognized in this process by a channel “ $p_{i}$ ”. An event triggers a transition from a state to another, a condition could be present on that transition, in addition to an action that could be executed by the agent during the transition. The transition is remote if the event is remotely triggered, or the action is remotely performed. Dispatching the events triggered by the environment in the diagram is represented by a process named “Events Wrapper (ER)”. Indeed, it sends the events “ $e_{i}$ ” one after one in a sequential manner, and in order to guarantee the run-to-completion of events (i.e. no event is sent until the previous is carried out), it uses a channel “rtc”. The evaluation of the conditions on transitions is represented by a process named “Condition Evaluator (CE)”. Effectively, it uses a series of channels “ $c_{i}$ ” to receive different evaluation requests, then according to the condition evaluation, it returns “true” or “false” to indicate that the condition is verified or not. To represent the execution of the different actions, a process “Action Handler (AH)” is used and it receives these actions by a series of channels “ $a_{i}$ ”. All previous processes are then assembled by a restricted composition to form the whole system “MSDname”. According to the execution of diagrams, these processes will evolve dynamically by message passing between themselves until the end of the execution.

Table 2
Tansformation of mobile statechart diagram to $\pi$ -calculus

Elements	$\pi$ -calculus	Comments
state $+$ simple transition	$\text{S1}(p_{1},e_{1},c_{1},a_{1})=p_{1}.\text{S1}(p_{1},e_{1},c_{1},a_{1})+e_% {1}.(\nu g)\overline{c_{1}}$ $<g>.g(y).([y=\text{true}]\overline{a_{1}}.\text{S2}(p_{1})+[y=\text{false}]% \text{S1}$ $(p_{1},e_{1},c_{1},a_{1}))$	Each transition could has an event $e_{1}$ , a condition $c_{1}$ , an action $a_{1}$ . $g$ is used to request the the condition value and $y$ is used to receive the response.
state $+$ remote transition	$\text{S1}(p_{1},\text{remote},a_{1})=p_{1}.\text{S1}(p_{1},\text{remote},a_{1}% )+\tau.$ $((\nu r_{1})\overline{\text{remote}}<r_{1}>\|r_{1}(a_{1})).\overline{a_{1}}.% \text{S2}(p_{1})$	remote is the channel used to request a remote communication. $r_{1}$ represents the intermediary used to retrieve the remote action.
state $+$ mobile transition	$\text{S1}(p_{1},\text{migrate})=p_{1}.\text{S1}(p_{1},\text{migrate})+\tau.(% \nu p_{2})$ $\overline{\text{migrate}}<p_{2}>.\text{S2}(p_{2})$	migrate is the channel used to request a migration. $p_{1}$ , $p_{2}$ represent the source and target platforms.
state $+$ $<<$ agentreturn $>>$ transition	$\text{Sn}(p_{m},\text{migrate})=p_{m}.\text{Sn}(p_{m},\text{migrate})+\tau.(% \nu p_{1})$ $\overline{\text{migrate}}<p_{1}>.\text{S1}(p_{1})$	The difference w.r.t. the last is that the agent uses the channel $p_{1}$ which represents the home platform.
platforms scheduler	$\text{PS}(\text{migrate},p_{1})=\overline{p_{1}}.\text{PS}(\text{migrate},p_{1% })+\text{migrate}(\text{newp}).$ $\text{PS}(\text{migrate},\text{newp})$	Control the agent movements, by communicating $p$ with the state process or receiving migration request.
events wrapper	$\text{ER}(\text{rtc},e_{1},\ldots,e_{n})=\tau.!\overline{e_{1}}.\overline{% \text{rtc}}.....\tau.!\overline{e_{n}}.\overline{\text{rtc}}.\text{ER}(\text{% rtc},$ $e_{1},\ldots,e_{n})$	Dispatches the events
conditions evaluation	$\text{CE}(\text{true},\text{false},c_{1},\ldots,c_{n})=\prod_{i=1}^{n}c_{i}(g)% .(\bar{g}<\text{true}>$ $+\bar{g}<\text{false}>).\text{CE}(\text{true},\text{false},c_{1},\ldots,c_{n})$	Receives conditions evaluation requests, and returns true or false.
actions handler	$\text{AH}(a_{1},\ldots,a_{n})=\sum_{i=1}^{n}a_{i}.\tau.\text{AH}(a_{1},\ldots,% a_{n})$	Executes the actions.
MSDs	MSDname $=$ ( $\nu\overline{\text{msd}}$ ) (S1 $\|$ PS $\|$ EW $\|$ AH $\|$ CE)	The system as a restricted composition of five processes. $\overrightarrow{\text{msd}}$ are different channels used.

With regards to necessary additional information from other diagrams, several questions must be answered to obtain a full and coherent $\pi$ -calculus specification from mobile statechart diagrams. Which class the agent specified by this diagram belongs to? How composing the processes corresponding to different mobile statechart diagrams? What an event is? Is it triggered locally or remotely? Does it has an order of production? What an action is? Is it carried out locally or remotely? How it is executed?

Using the mobile class diagram and the mobile collaboration diagram, answers to the previous inquiries could be provided. In fact, each agent specified by this diagram belongs to a class in the mobile class diagram, this last gives more information about the behaviour of the agent in its methods in addition to its relationship with the other agents.

The mobile collaboration diagram allows composing the processes corresponding to different mobile statechart diagrams by assembling them in one process. This what covers the missing part in each mobile statechart diagram which supposed communicating with fictive processes during its formalisation. Therfore, this gives a complete vue of the interacting entities of the system. Events, also, are described in details in the mobile collaboration diagram (messages sending/receiving and their order). Actually, the mobile collaboration diagram identifies the events that a process Events Wrapper (ER) gets in each communicating statechart diagram. The order is related to the message number, using a FIFO strategy (first come first served).

Actions are described in details in the mobile class diagram as methods. Actually, A method tells us with details how the action will executed, for example if the action needs some arguments and if it returns something as results of the execution. So, the mobile class diagram gives details to the Action Handler (AH) how to execute the actions.

4.3.2 The graph grammar

The proposed graph grammar is composed of twenty-six (26) rules used to implement the semantic rules above. In our case, the actions of the rules generate the corresponding $\pi$ -calculus expression to the sub-graph matched using the Python code according to the semantics rules. The LHSs of the grammar are composed only by elements of the mobile statechart diagram, while the the RHSs have besides the elements of the mobile statechart diagram, the elements needed from the other diagrams to generate the adequate code. The priorities indicate the order of execution of the rules by the transformation engine. The word ANY means any value on that element is accepted in translation, the word COPIED means that the value of the element will be copied from the LHS or specified by Python code.

Figure 6 shows six essential rules which we have estimated that they are sufficient to well understand the automatic mapping. The other rules are very similar to the rules presented. When the graph grammar executes, the model is a blend of the three different diagrams, this is normal since what interest us is the rich $\pi$ -calculus specification generated after the execution.

Figure 6.

The proposed graph grammar.

All the rules of the formalization have been implemented and the graph grammar will automatically encode in the $\pi$ -calculus each specification (which consists of mobile class diagrams, mobile statechart diagrams and mobile collaboration diagrams) modeled in the integrated tool. The generated $\pi$ -calculus specification will be then automatically imported into a specialized tool (i.e. The MWB) for analysis purposes.

Initial Action: used to start the execution of the graph grammar by preparing the file “picalculus.txt” that will contain the generated $\pi$ -calculus code.

Rule 1: this rule translates the LHS composed of a transition between an initial pseudo-state and a state to their corresponding $\pi$ -calculus process expressions. It picks that sub-graph, then in the RHS of the rule, we need more information (which class the agent belongs to) from the mobile class diagram to generate the corresponding $\pi$ -calculus code in the action of the rule.

Rule 2: this rule translates the LHS composed of a simple transition between two states to the corresponding $\pi$ -calculus process expressions. To do so, in the (RHS) of the rule, we need the action description from the mobile class diagram, and the event description from the mobile collaboration diagram (the particular order given by the sequence number attached to the interaction).

Rule 3: this rule translates the LHS composed of a remote transition between two states to the corresponding $\pi$ -calculus process expressions. To do so, in the (RHS) of the rule, we need the details of the remote action and the event description from the mobile class and collaboration diagrams respectively.

Rule 4: this rule translates the LHS composed of a mobile transition between two states to the corresponding $\pi$ -calculus process expressions. To do so, in the (RHS) of the rule, we need the event description, the action description, and the interaction location description.

Rule 5: this rule translates the LHS composed of an $<<\textit{agnetreturn}>>$ transition between two states to the corresponding $\pi$ -calculus process expressions. To do so, in the (RHS) of the rule, we need the event description, the action description, and a self-loop interaction to describe the return of the agent (from the mobile collaboration diagram).

Rule 6: this rule translates the LHS composed of a transition between a state and a final pseudo-state to their corresponding $\pi$ -calculus process expressions. To do so, in the RHS of the rule, we need more information how the agent finishes its execution (methods from the mobile class diagram).

Final action: used to end the execution of the graph grammar by closing the file “picalculus.txt”.

Figure 7.

Details of Rule 4 with condition and action.

The previous rules show how the elements of the mobile state diagram bind to some elements of the others diagrams, i.e. class and collaboration diagrams, in order to retrieve necessary additional information. Moreover, the generation of the $\pi$ -calculus code is carried out in parallel in the action section of all these rules. To understand how the obtained blended diagram is translated into $\pi$ -calculus, Fig. 7 presents in details “Rule 4”, the other rules have the same principle to the one presented here.

5. Example

5.1 Mobile Voting System (MVS)

As an example, a Mobile Voting System (MVS) specified in M-UML from [25] is taken. The system is composed of multiple type of agents: VC (vote collector), VM (vote manager), VOs (voters), Logger. Only VC is mobile, the others are stationary agents. In election time, the mobile agent VC gets a list of voters from a stationary agent VM (which mandates this VC), and visits the voters stations VO’s, which already have the list of candidates, in order to collect the votes results and forwards them to the VM that mandated the VC in question. The system can be expanded to have more agents of different types, but for reasons of simplification, four (04) agents are taken (one of each type).

Assuming that the designer has provided an M-UML specification composed of a mobile class diagram, a mobile statechart, and a mobile collaboration diagram. There is only one mobile statechart diagram that specifies the behaviour of the class VC of the mobile class diagram, the other classes do not have any associated statechart.

Figure 4b (or see Fig. 8 where all diagrams are gethered) shows the class diagram, it involves mobile and non-mobile classes. The class VC is used to instanciate mobile agents. The class VM is affected because it includes the method GetVotersList which is invoked by the class VC’s mobile agent. The instances of VM and VO are not mobile. The diagram shows the relations between VO, VC and the VM agents. The Logger class is associated with the VC class since it contains the method logList invoked remotely by a mobile agent of class VC.

Figure 8.

Muli-paradigm modelling of the MVS in the developed tool.

Figure 5b (or see Fig. 8 where all diagrams are gethered) illstrates an example of a collaboration diagram. The first and second interactions are localized interactions. The third interaction shows that VC (a mobile agent) is remotely interacting with the Logger agent at VM’s platform. The fourth interaction indicates the move of VC to VO’s platform to locally interact with a voter VO. The fifth interaction shows the return of the VC to its home platform.

Figure 3b (or see Fig. 8 where all diagrams are gethered) shows a state behaviour of the mobile agent VC. Initially, the VC is at its home platform in the state ReadyToMove (RTM) waiting to get an event StartVotingProcess. It then moves by a mobile transition to the state VotingManagerReached (VMR) located at another platform. At VMR, the mobile agent used to get the list of voters by performing an action GetVotersList and moves by a normal transition to the state WaitForList (WFL), where it waits for the list. At WFL, the mobile agent waits to receive an event VotersList, it then executes the LogList action while interacting remotely with the Logger agent and moves by a remote transition to the state ReadyToCollectVotes (RCV). At RCV, the mobile agent executes the action GetVote and moves by a mobile transition to the state WaitingForVote (WFV) at the first VO platform. At WFV, the mobile agent makes a $<<$ agentreturn $>>$ transition in order to return to its home platform.

The full M-UML design of the Mobile Voting System MVS created in our tools is shown in Fig. 8, since the AToM ${}^{3}$ is a multi-paradigm tool, it offers the capability of describing all the models at the same environment.

Thus, this M-UML design is translated into $\pi$ -calculus by applying the graph grammar on that design, and consequently a full enriched $\pi$ -calculus specification is obtained. This last describes espicially the behaviour of the mobile class VC and its interaction with the environment.

5.2 The generated code

The generated specification in Snippet 1 is presented with explanation, the MWB format is used which means that the restriction $\nu$ is replaced by ${}^{\wedge}$ , the output action x is replaced by ’x, the internal action $\tau$ is replaced by t and the continuation character as $\backslash$ .

agent System

=

’vmstartvotingprocess.’rtc.0

|

|

|

|

|

The process System represents the behaviour of the whole system. It starts the execution by sending the channel “vmstartvotingprocess” then it behaves as the null process. In parallel, it launches the execution of the processes VM, VO, VL, PS, and VC. These last will evolve dynamically during the execution by message passing.

agent VM

=

{}^{\wedge}

m ’k

{}_{\text{VM}}

<

>

.VM

{}_{1}

(m)

agent VM

{}_{1}

(m)

=

vmgetvoterslist.’vmvoterslist.’rtc.0

agent VO

=

{}^{\wedge}

o ’k

{}_{\text{VO}}

<

>

.VO

{}_{1}

(o)

agent VO

{}_{1}

(o)

=

vogetvote.t.0

agent VL

=

{}^{\wedge}

l ’k

{}_{\text{VL}}

<

>

.VL

{}_{1}

(l)

agent VL

{}_{1}

(l)

=

remote(loggerloglist).t.0

The processes VM, VO, VL describe the behaviour of the vote manager VM, the voters VO and the logger Logger respectively. A remark is that there is restricted provided details about their behaviour, the only available information are captured from the mobile class and the mobile collaboration diagram. Our approach gathers the maximum available information from these diagrams. In VM, A new channel “m” is created and sended using “k

{}_{\text{VM}}

” to indicate which manager is concerned by the execution in our system, then it behaves as the process VM

{}_{1}

(m). This last, waits to receive the “vmgetvoterslist” channel, after that it sends the “vmvoterslist” channel followed by the rtc channel and it dead. In VO, A new channel “o” is created and sended using “k

{}_{\text{VO}}

” to indicate which voter is concerned by the execution, then it behaves as the process VO

{}_{1}

(o). This last, waits to receive the “vogetvote” channel to dead. In VL, a new channel “l” is created and sended using “k

{}_{\text{VL}}

” to indicate which logger is concerned by the execution, then it behaves as the process VL

{}_{1}

(l). This last, waits to receive the “loggerloglist” channel using the “remote” channel to dead.

agent PS(migrate, p1)

=

’p1.PS(migrate, p1)

+

migrate(newp).PS(migrate, newp)

agent VC

=

{}^{\wedge}

c ’k

{}_{\text{VC}}

<

>

.VC

{}_{1}

(c)

agent VC

{}_{1}

(c)

=

(

{}^{\wedge}

p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote) RTM(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

agent RTM(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

=

p1.RTM(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist,vogetvote)

+

\backslash

vmstartvotingprocess.’migrate

<

>

.VMR(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

agent VMR(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

=

p2.VMR(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

+

\backslash

’vmgetvoterslist.WFL(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

agent WFL(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

=

p2.WFL(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

+

\backslash

vmvoterslist.’loggerloglist.RCV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

agent RCV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

=

p2.RCV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

+

\backslash

’vogetote.’migrate

<

>

. WFV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

agent WFV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

=

p3.WFV(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

+

\backslash

(

{}^{\wedge}

p1)’migrate

<

>

.RTM(p1, p2, p3, migrate, vmstartvotingprocess, vmvoterslist, vmgetvoterslist, loggerloglist, vogetvote)

The process “PS” is the platform scheduler; it is used to model the mobility from a platform to another by communicating with the current process representing the agent or receiving a migration request through the channel “migrate”.

The process models the agent VC behaves as having five states “RTM, VMR, WFL, RCV, WFV”. This process evolves from a state to another every time a transition is performed. There are two mobile transitions “RTM

\to

VMR and RCV

\to

WFV”, a simple transition “VMR

\to

WFL”, a remote transition “WFL

\to

RCV” and an

<<

agentreturn

>>

transition “WFV

\to

RTM”.

The evolution of all precedents processes will be done according to the semantic rules defined above.

Snippet 1. Generated sample code

5.3 Analysis

At this stage, a derived specification of $\pi$ -calculus code is provided. Indeed, it specifies the behaviour of a subset of mobile UML diagrams with satisfactory details. It is then imported into the MWB tool [27] to start the automatic verification. Thus, one can verify several types of properties as already said due to the rich theory of the $\pi$ -calculus (see Fig. 9).

For example, one can verify standard properties such as deadlock and livelock of the agents VM, VO, VL, VC during their execution. Since there is one VM, one VO, one VL and one VC, their instanciation from their classes give VM1, VO1,VL1, VC1. The MWB shows that VM1, VO1, VL1 could deadlock, this is evident since their definitions contain states that have no out-going transitions due to the absence of their details of execution (expected to be modeled by statecharts, but unfortunately not provided by the designer). In contrast, the agent VC1 can not deadlock, the process PS and System also can not deadlock. The deadolock is checked in MWB by the command “deadlocks”.

Also, special properties, described by mu-calculus modal logic [12], could be verified, such as the following property on the PS process: for example, using the operator with the largest fixed point “max”, it can be shown that PS (the process which guarantee mobility of agents) will be always able to synchronize on an output port “p1” or on an input port “migrate”.

$\displaystyle\text{(max W. (([`p1]TT {\&} [i]W)}|\text{($<$migrate$>$TT {\&} [% `i]W)))}$ (1)

This safety property has two parts related by a disjonction: ([‘p1]TT & [i]W) expresses the fact that PS can always make an output on “p1”, and all the input actions that it is able to do will bring it to a state where W is true again. ( $<$ migrate $>$ TT & [‘i]W) expresses the fact that PS can always make an input on “migrate” and all the output actions that it is able to do will bring it to a state where W is true again.

Figure 9.

Verification using MWB.

Figure 9 starts by importing the generated $\pi$ -calculus specification, then the debugging level of MWB is increased to see more details about the deadlock (what paths conduct to it) of processes VM1, VO1, VL1,VC1, PS and System. The MWB model checker is also invoked to check a mu-calculus property which is verified after nine inferences.

6. Discussion

This section provides some critical discussion points. The approach commonalities with the related work in the literature are especially the philosophy of combination of a graphical intuitive language to model a type of systems, and a formal rigorous method to verify them, such as in [9, 18, 19, 23, 28]. However, there are a lot of differences with regards to the work done.

The main contribution of this paper is the idea of using three views of M-UML at the same time, contrary to [2, 16], to enable full modelling of mobile agent based software systems (from different views to accumulate information), and transforming them together to $\pi$ -calculus to generate a full specification for verification purpose. Adopting the multi-paradigm tool AToM ${}^{3}$ to realize the approach has provided a lot of benefits, as stated in [11, 15, 17], since it comprises all the necessary mechanisms, such as metamodelling and graph grammars which allow building diagrams and handling them. Also, adopting $\pi$ -calculus was a great choice, due to its rich thery and tools in comparison of the semantic domains adopted in [16]. Actually, if offers diverse verification techniques as we saw, which gives some kind of ease in tackling such problems. Besides what was presented in the example, equivalence checking is also a very interesting technique among other verification capabilities given by $\pi$ -calculus. In fact, one can take other systems and generates their $\pi$ -calculus specifications (as already done for MVS system), then proceeds to verify if the observed behaviour of two systems is the same by equivalence checking of their corresponding $\pi$ -calculus specifications. Another interesting point is enabling the verification even if the designer does not provide enough information in diagrams, as shown in the last presented example where only the statechart of the VC is described (the others are omitted), and despite that we proceeded to verification. Thus, with our approach, a minimum of automatic verification could be done, and whenever the designer provides more information in the diagrams, whenever getting more adequate results and more verification possibilities. This is not possible with the presented works in the literature.

As cons of the approach, some users and although the UML simplicity, need some training in desining with that language, and the approach can’t garantee anything if first of all the user couldn’t provide correct conceptions. In fact, This is a common problem with all approaches which adopt UML, including the presented works in the literature. Also, we can evoke the problem of state explosion in model checking with MWB (in reality it’s not just with this tool), and this is what could hinders tackling modelling and verification of big complex systems. Another lack is that MWB doesn’t provide countre-examples when you got unverified properties, so it could be difficult for lambda users to understand and react to detected problems. In [9], we can not even talk about that because there is no support tool. Although that, since the MWB tool is based on “on-the-fly” approach, it gives more performance than other tools adopted in the related work (e.g. [11, 15, 17]), especially when big models (i.e. big systems) are manipulated, but nevertheless there is still work to be done.

Regarding applying our proposal on real world problems, it could be used in modelling and verification of a large range of mobile agent-based applications, since the general-purpose deliberately adopted during the development of the framework. Such real experimentations will be the subject of future work.

Finally, despite what we have already enumerated as limitations, we are sure that the approach makes a step forward in providing a real practical tool used by quite many users for specifying and developing such systems.

7. Conclusion

In this paper, a framework for modelling and verification of mobile agent based-software systems has been developed. A combined meta-modelling and graph grammar approach is adopted and the multi-paradigm tool AToM ${}^{3}$ is chosen to realize this framework. Different types of M-UML models (mobile class diagram, mobile statechart diagram, mobile collaboration diagram) are used as a source, and the target common formalism adopted in the contribution is the $\pi$ -calculus. This formalism offers the theory and tools to verify the properties we are interested in the system.

Other diagrams of mobile UML (such as mobile activity diagrams) could be added to our framework, and this is what we are working on currently. Future work could includes developing an extended framework that contains more diagrams. By this way, we will guarantee that all views of the mobile agent system are covered. Another issue, we are currently working on, is hiding the verification process by extending MWB to simplify the verification task, such as returning a counter-example, so that a lambda-user can use easily our approach.

Footnotes

https://en.wikipedia.org/wiki/Robin_Milner.

Author’s Bios

Aissam Belghiat is an assistant professor at the Department of Computer Science, University of Jijel, Algeria. He is author of many articles in International Conferences and Journals. He has prepared and taught also several courses especially in Software Engineering such as Formal Methods and Model Transformation. His research interests include mobile agents, web services, modeling with UML, formal methods, model transformation, system verification, ontologlies and all aspects related to Software Engineering.

Allaoua Chaoui is with the department of computer science, Faculty of Engineering, University Mentouri Constantine, Algeria. He received his Master degree in Computer science in 1992 (in cooperation with the University of Glasgow, Scotland) and his PhD degree in 1998 from the University of Constantine (in cooperation with the CEDRIC Laboratory of CNAM in Paris, France). He has served as associate professor in Philadelphia University in Jordan for five years and University Mentoury Constantine for many years. During his career he has designed and taught courses in Software Engineering and Formal Methods. Allaoua Chaoui has published many articles in International Journals and Conferences. He supervises many Master and PhD students. His research interests include Mobile Computing, formal specification and verification of distributed systems, and graph transformation systems.

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

1. Introduction

2. Literature review

3. Preliminaries

3.1 Mobile UML (M-UML)

3.2 π -calculus

3.3 Graph grammars in AToM 3

Table 1 Reduction semantics of the π -calculus

4. The proposed modeling and verification framework

4.1 The architecture of the framework

4.2.1 Mobile statechart diagram meta-model

4.3.1 Semantics rules

Table 2 Tansformation of mobile statechart diagram to π -calculus

5.1 Mobile Voting System (MVS)

5.3 Analysis

7. Conclusion

Footnotes

Author’s Bios

References

3.2 $\pi$ -calculus

3.3 Graph grammars in AToM ${}^{3}$

Table 1
Reduction semantics of the $\pi$ -calculus

Table 2
Tansformation of mobile statechart diagram to $\pi$ -calculus