Activity Diagrams have been used largely in modeling the behavior of control ow and data ow. Unfortunately, they su er from lack of formal semantics due to its semi-formal nature as all UML diagrams, which prohibits any task of automatic veri cation. The use of formal methods has been adopted largely, but their interpretation generates another problem. Thus, this paper presents a user-friendly framework that is enabling intuitive visual modeling of systems using UML activity diagrams, and their veri cation using pi-calculus formal language, without the obligation to master this formal language.
UML (Uni ed Modeling Language) [OMG17] is considered as the standard visual modeling language that is used to specify, visualize, construct, and document artifacts in software systems. Its two main objectives are the modeling of systems using object-oriented techniques, from design to maintenance, and the creation of an abstract language understandable by humans and interpretable by machines. Although UML is a rich language, with an open and widely used notation, its models still need to be checked to ensure that the behavior speci ed in these models is correct, and exactly meets the functional requirements of the system. This fact is due to the graphic and semi-formal nature of the UML language i.e. to its semantics which is not formally speci ed.
On the other hand, pi-calculus [Mil99] is a theoretical formal language that provides powerful tools for analysis and veri cation. It can be used to verify correctness of properties of a model, or check equivalence between two models.
Therefore, UML and pi-calculus have complementary characteristics; UML can be used for intuitive visual modeling while pi-calculus can be used for veri cation.
In this paper, we propose an approach that automates the mapping between UML activity diagrams towards pi-calculus. This work is inscribed in the context of the MDA (Model Driven Architecture) [OMG04] where model transformation is used and exploited. More precisely, the graph transformation, which is based on meta-modeling and graph grammar, is used to realize the model transformation as activity diagrams are graphs.
Building a modeling tool from scratch has never been a trivial task; on the contrary it was always difcult and hard. Meta-modeling approach has shown positive performances in dealing with this problem, because it gives freedom and easiness in modeling the formalisms themselves. A formalism model that contains enough information allows the automatic generation of a tool for constructing models that conforms to the syntax and semantics of the described formalism. The graph grammar is used then to transform the models into pi-calculus and returns an understandable analysis feedback to the user. We have used AToM3 (A Tool for Multi-formalism Meta-Modeling) [ATo02]; which is a tool that provides the mechanisms allowing the realization of these concepts.
The rest of the paper is organized as follows. In Section 2, some related works are exposed. In Section 3, we brie y present UML activity diagram, pi-calculus and graph transformation. In Section 4, the proposed framework is explained. In Section 5, an example is presented. Section 6 concludes the paper and gives some perspectives. 2
The literature contains a broad range of works regarding giving formal semantics to UML diagrams in general and Activity Diagrams speci cally. Among others we choose some works which are very close to ours. In [BCR00], the authors use ASM (Abstract State Machine) for representing behavior semantics of activity diagrams. In [Rod00], an FSP (Finite State Processes) formalism is adopted to formalize activity diagrams. In [BD00a, BD00b], the CSP (Communicating Sequential Processes) formalism is used to specify the execution semantics of activity diagrams. In [EW02] an activity hypergraph and a Kripke structure have been used as intermediate representations when transforming an activity diagram into the model checker NuSMV input language according to STATEMATE semantics. The last work has been enhanced in [Esh06] by adopting both STATEMATE and UML statechart semantics. Other works use Petri-nets and their extensions (Colored Petri-nets, High-level Petri-nets) to formalize activity diagrams such as in [SH05, Sto04a, Sto05, Sto04b, BG03].
There is also some works use pi-calculus as semantic domain to give formal semantics to activity diagrams such as in [Lam08] where the authors aim to check a model against its speci cations expressed in modal mu-calculus, and also in [YZ04], where a full formal framework is proposed using pi-calculus. The automation of the translations is not provided.
To build automation translations, some works adopted CASE tools such as AToM3 tool which has been used with success in those projects. In [GD03], an AToM3 integrated framework has been developed for the veri cation of UML models using Petri Nets. They build meta-models for an UML design (composed of Class, Statecharts and Sequence diagrams) in addition to a Petri Nets meta-model. Then, they use graph grammars to translate the former to the later which allow their veri cation by model checking. In [Ker+10], the authors have used an UML design composed of statechart and collaboration diagrams to propose an AToM3 integrated approach for modeling and analysis of such models. They have used graph transformation in mapping the diagrams into Colored Petri net models. In [CEC12], the authors have used a subset of UML diagrams to develop an AToM3 integrated framework for their model checking by transforming them into a rewriting system expressed in the Maude language. Other contributions deserve to be cited such as [Bel+14], [BC16] and [BCB16].
We notice that all previous contributions have not taken into account that the user is not specialized in most cases, and he does not master these formal languages, in addition most of them do not even provide automation, what hinders their usage. Thus, in contrast, we develop in this work an AToM3-based framework that automates the mapping of activity diagrams into pi-calculus. In addition we try to drive away the veri cation task from users by interpreting feedback analysis results. The AToM3 tool is chosen because it o ers the capabilities we need to realize our ideas. 3 3.1
The UML activity diagram [OMG17] is used for modeling control ow and data ow. It gives an explanation of the sequence of activities and actions speci c to an operation or a use case. It provides a set of elements that allow a very rich expression of any sequence in a system, its notation is relatively close to the state-transition diagram in its presentation, but its interpretation is signi cantly di erent. The activity diagram is essentially composed of activities and transitions. An activity speci es a behavior described by an organized sequencing of units whose basic elements are actions. The most common types of actions are: call operation, call behavior, send, accept event, accept call, reply, create, destroy, and raise exception. Each of them is used to represent the adequate behavior. A transition materializes the transition from one activity to another, it is triggered when the source activity is completed and immediately causes the start of the target activity. Therefore, transitions allow specifying sequence of treatments and de ne the control ow. Activity diagrams provide the mechanism for partitions, called swimlanes which allow organizing the nodes of activities by making regroupings. 3.2
The pi-calculus [Mil99] is a formal language that has solid mathematical bases. It is a computing model that is used to represent concurrent and mobile systems by the expression of interactions between evolving processes, its two basic concepts are Names and Processes. A Name represents channels(ports), variables, data while a Process represents a communicating entity in a system. The syntax of the pi-calculus process expression is given in Table 1: Graph transformation is one of the approaches used to implement model transformation. It consists on mapping a source graph into another target graph, by using a combined technique of meta-modeling and graph grammar. AToM3 [ATo02] is a powerful model transformation tool that implements the ideas of graph transformation.
The meta-modeling allows specifying the abstract syntax (the relationships between the elements) of any formalism, and its concrete syntax (the graphical notation that must be respected by models).
Graph grammars [Roz97] are generalization of Chomsky grammars for graphs. In AToM3, a graph grammar is composed of an initial action, multiple rules and a nal action. Initial and nal actions are used to provide necessary information before and after the execution of the rules. Each rule has two graphs; one on its left called the LHS (Left Hand Side) and another one on its right called the RHS (Right Hand Side). A rule is evaluated by comparing its LHS with a zone in an input graph (called host graph). If a matching is found, the rule will be executed and the corresponding matching sub-graph in the host graph will be replaced by the rule RHS. Furthermore, a rule may also have a condition that must be satis ed to apply the rule, as well as actions to be performed when the rule is carried out. The tool has a rewriting system that iterates applying the matching rules in the graph grammar to the host graph, until no rule is applicable. The rules are also ordered in this tool by a user-assigned priority (higher to lower).
In our framework, a combined meta-modelling and graph grammar approach is adopted to build an integrated tool using the AToM3 (see Figure 1). The approach consists of two essential tasks; rstly, we needed to propose a meta-model for activity diagrams to generate an AToM3 integrated environment which supports the visual modeling of these diagrams. Secondly, we have proposed and developed a graph grammar which gives us for each activity diagram modeled in the tool its corresponding pi-calculus process expression. This last is uploaded immediately in the mobility workbench (MWB) [VM94] to start the veri cation task. Thirdly, the results of the veri cation will be exported to the graph grammar (a feedback) that try to identify the problem found by interpreting these results and makes a sign on the diagram itself (the deadlock as example). Activity diagrams must be provided with formal semantics in order to be able to verify any aspect of the behavior [Rod00]. To overcome this problem the pi-calculus can be used for the veri cation by a transformation approach of the activity diagrams into picalculus (Table 2) Our meta-model is composed of 8 classes and 7 associations developed by the meta-formalism (CDclassDiagramsV3) in order to have an AToM3-based tool which o ers the necessary tools to model the activity diagrams (see Figure 2).
After we have come to model our meta-model, only its generation remains. The generated meta-model contains the set of classes modeled as buttons that are ready to be used for a possible modeling of an acThe construction of graph grammar rules is an important step in the process of implementing a graph transformation. Indeed, it requires a good understanding of both languages. Thus, we have inspired the semantic rules from [Lam08].
Thus we propose the graph grammar (AD2Picalculus) composed of an initial action, 30 rules, and a nal action. It should be noted that due to space constraints we cannot present all the rules, so we choose some rules among others and we join them with the Python code used for generating automatically pi-calculus code.
Role: In the initial action of the graph grammar we have created a le with sequential access named "picalculus.txt" to store the generated pi-calculus code.
Activity diagrams environment under
Role: In the nal action of the graph grammar, we close the le "picalculus.txt".
Rule 1 : Initial Node mapping Name : Initial2Initial Priority : 1
Role: This rule makes it possible to transform an initial node that links by an action to the pi-calculus, in this rule we return the name of the initial node and the name of the outgoing arc, In the condition of the rule we test if the node is already transformed, otherwise the action of the rule opens the le "picalculus.txt" and adds the class in the pi-calculus code (see Figure 4).
Similar rules are initial2decision, initial2fork, initial2merge, they are described in Figure 5. The difference is in the code python used to generate the picalculus code as already seen in table2.
Rule 2 : Action mapping
Name : Action2picalcul Priority : 2
Role:This rule allows transforming an Action with the incoming arc from an action and the outgoing arc that ends to an action, in this rule we return the name of the action and the name of the incoming and outgoing arc (see Figure 6). Examples of similar rules are Action2decision, Action2Fork, Action2join, Action2merge, Action2 nal, ...etc.
Rule 3 : Fork mapping Name : fork2picalcul Priority : 5
Role:This rule enables transforming a fork node that is linked by a single incoming arc from an action and outgoing arcs that end to actions (see Figure 7).
An example of a similar rule is join2picalcul. It is applied to locate a join node, and transforms it to picalculus code according to the semantic rules already described in Table 2.
Rule 5 : Merge mapping Name : merge2picalcul Priority : 3 Role:This rule transforms a merge node with two or more incoming arcs from an action and an outgoing arc that ends to an action (see Figure 8).
An example of a similar rule is decision2picalcul. It is applied to locate a decision node, and transforms it to pi-calculus code according to the semantic rules already described in Table 2. 5
In order to concretize the usefulness of the de ned graph transformation, we tried to apply it to the simple example of the activity diagram presented in Figure 9. It should be noted that this example does not claim to be exhaustive, but it includes some important elements of an activity diagram such as: action, fork, join..etc.
The generated pi-calculus code is described in Figure 10:
If we remove the transition between the action "delliverorder" and the nal node, we create a deadlock in the diagram. Thus, the reloaded pi-calculus code will be similar except for the process (agent):
agent delliverorder(x6,x7) = x6.t.delliverorder(x6,x7)
Our tool will analyze the code using MWB, it immediatly detects the deadlock (a state that has no outgoing transitions) and the process concerned. The nal action of the graph grammar points out the problem by coloring the the corresponding element of the deadlocked process in the graph of the diagram (see Figure 11). The result of our work is an automatic approach that enables visual modeling of systems behavior using UML activity diagrams and their veri cation using picalculus. The proposed approach is based on the graph transformation, and it is carried out using the AToM3 tool. The meta-modeling is used to de ne an environment for activity diagrams while the graph grammars are used to automate the translation and the analysis feedback. We saw in the last example the deadlock property, some other properties need more advanced feedback mechanisms to be understandable such as counter-examples. In future work, we plan to enable such mechanism by interpreting feedback analysis using Sequence Diagrams depicted in AToM3. In addition, we intend formalizing and integrating in our framework other notational elements such as expansion region and interruptible activity region. We plan also to apply our approach to a wider range of realworld critical systems in order to experiment its performance. [Mil99] (OMG), (MDA), [ATo02] AToM3 home page, (online) available at: http://atom3.cs.mcgill.ca/, 2002. [BCR00] E. Borger, A. Cavarra, and E. Riccobene. An ASM Semantics for UML Activity Diagrams. 8th International Conference, AMAST 2000, volume 1816 of LNCS, pages 293{308.
Springer-Verlag, 2000. [Rod00] R. W. S. Rodrigues. Formalising UML Activity Diagrams using Finite State Processes, UML2000 workshop.2000. [BD00a] C. Bolton and J. Davies. On giving a behavioral semantics to activity graphs, in UML 2000 Workshop Dynamic Behavior in UML Models: Semantic Questions, 2000. [BD00b] C. Bolton and J. Davies, Activity graphs and processes, in 2nd Int. Conf. Integrated Formal Methods, LNCS 1945, 2000, pp. 77-96. [EW02] R. Eshuis and R. Wieringa. Veri cation support for workow design with UML activity graphs, in 22nd Int. Conf. on Software Engineering, ACM Press, 2002, pp. 166-176. [Esh06] R. Eshuis. Symbolic model checking of UML activity diagrams, ACM Trans. Software Engineering and Methodology 15(1), 2006.
H. Storrle and J. H. Hausmann. Towards a formal semantics of UML 2.0 activities, in German Software Engineering Conf. 2005, 2005. [SH05] [Sto05] [Sto04a] H. Storrle. Semantics of Control-Flow in UML 2.0 activities, in 2004 IEEE Symp. Visual Languages and Human Centric Computing, IEEE Computer Society, pp. 235-242, 2004.
H. Storrle. Semantics and veri cation of data ow in UML 2.0 activities, Electronic Notes in Theoretical Computer Science 127,35-52, 2005. [Sto04b] H. Storrle. Structured nodes in UML 2.0 activities, Nordic Journal of Computing 11(3) (2004) 279-302. [BG03] J. P. Barros and L. Gomes. Actions as activities and activities as Petri nets, in Workshop on Critical Systems Development with UML, 2003. [Lam08] V.S.W. Lam. On pi-calculus semantics as a formal basis for UML activity diagrams. International Journal of Software Engineering and Knowledge Engineering 18(4), 541-567, 2008. [YZ04]