A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose Aissam Belghiat1,2 1 Department of Computer Science University of Mohamed Seddik Benyahia-Jijel, Jijel, Algeria aissam.belghiat@univ-jijel.dz Allaoua Chaoui2 2 MISC Laboratory University of Constantine 2-Abdelhamid Mehri, Constantine, Algeria allaoua.chaoui@univ-constantine2.dz of an abstract language understandable by humans and interpretable by machines. Although UML is a Abstract rich language, with an open and widely used notation, its models still need to be checked to ensure that the Activity Diagrams have been used largely in behavior specified in these models is correct, and ex- modeling the behavior of control flow and data actly meets the functional requirements of the system. flow. Unfortunately, they suffer from lack of This fact is due to the graphic and semi-formal nature formal semantics due to its semi-formal na- of the UML language i.e. to its semantics which is not ture as all UML diagrams, which prohibits any formally specified. task of automatic verification. The use of for- On the other hand, pi-calculus [Mil99] is a theoret- mal methods has been adopted largely, but ical formal language that provides powerful tools for their interpretation generates another prob- analysis and verification. It can be used to verify cor- lem. Thus, this paper presents a user-friendly rectness of properties of a model, or check equivalence framework that is enabling intuitive visual between two models. modeling of systems using UML activity dia- grams, and their verification using pi-calculus Therefore, UML and pi-calculus have complemen- formal language, without the obligation to tary characteristics; UML can be used for intuitive vi- master this formal language. sual modeling while pi-calculus can be used for verifi- cation. Keywords: UML, Activity Diagram, Graph transfor- In this paper, we propose an approach that auto- mation, Verification, Pi-calculus mates the mapping between UML activity diagrams towards pi-calculus. This work is inscribed in the 1 Introduction context of the MDA (Model Driven Architecture) UML (Unified Modeling Language) [OMG17] is con- [OMG04] where model transformation is used and ex- sidered as the standard visual modeling language that ploited. More precisely, the graph transformation, is used to specify, visualize, construct, and document which is based on meta-modeling and graph grammar, artifacts in software systems. Its two main objectives is used to realize the model transformation as activity are the modeling of systems using object-oriented tech- diagrams are graphs. niques, from design to maintenance, and the creation Building a modeling tool from scratch has never been a trivial task; on the contrary it was always dif- Copyright c by the paper’s authors. Copying permitted for ficult and hard. Meta-modeling approach has shown private and academic purposes. positive performances in dealing with this problem, In: Proceedings of the 3rd Edition of the International Conference on Advanced Aspects of Software Engineering because it gives freedom and easiness in modeling the (ICAASE18), Constantine, Algeria, 1,2-December-2018, pub- formalisms themselves. A formalism model that con- lished at http://ceur-ws.org tains enough information allows the automatic gener- Page 107 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 ation of a tool for constructing models that conforms low their verification by model checking. In [Ker+10], to the syntax and semantics of the described formal- the authors have used an UML design composed of ism. The graph grammar is used then to transform the statechart and collaboration diagrams to propose an models into pi-calculus and returns an understandable AToM3 integrated approach for modeling and analy- analysis feedback to the user. We have used AToM3 sis of such models. They have used graph transfor- (A Tool for Multi-formalism Meta-Modeling) [ATo02]; mation in mapping the diagrams into Colored Petri which is a tool that provides the mechanisms allowing net models. In [CEC12], the authors have used a sub- the realization of these concepts. set of UML diagrams to develop an AToM3 integrated The rest of the paper is organized as follows. In framework for their model checking by transforming Section 2, some related works are exposed. In Section them into a rewriting system expressed in the Maude 3, we briefly present UML activity diagram, pi-calculus language. Other contributions deserve to be cited such and graph transformation. In Section 4, the proposed as [Bel+14], [BC16] and [BCB16]. framework is explained. In Section 5, an example is We notice that all previous contributions have not presented. Section 6 concludes the paper and gives taken into account that the user is not specialized in some perspectives. most cases, and he does not master these formal lan- guages, in addition most of them do not even provide 2 Related Works automation, what hinders their usage. Thus, in con- trast, we develop in this work an AToM3-based frame- The literature contains a broad range of works regard- work that automates the mapping of activity diagrams ing giving formal semantics to UML diagrams in gen- into pi-calculus. In addition we try to drive away the eral and Activity Diagrams specifically. Among others verification task from users by interpreting feedback we choose some works which are very close to ours. In analysis results. The AToM3 tool is chosen because it [BCR00], the authors use ASM (Abstract State Ma- offers the capabilities we need to realize our ideas. chine) for representing behavior semantics of activity diagrams. In [Rod00], an FSP (Finite State Processes) 3 Background formalism is adopted to formalize activity diagrams. In [BD00a, BD00b], the CSP (Communicating Sequen- 3.1 UML Activity Diagram tial Processes) formalism is used to specify the exe- The UML activity diagram [OMG17] is used for mod- cution semantics of activity diagrams. In [EW02] an eling control flow and data flow. It gives an explana- activity hypergraph and a Kripke structure have been tion of the sequence of activities and actions specific used as intermediate representations when transform- to an operation or a use case. It provides a set of ing an activity diagram into the model checker NuSMV elements that allow a very rich expression of any se- input language according to STATEMATE semantics. quence in a system, its notation is relatively close to The last work has been enhanced in [Esh06] by adopt- the state-transition diagram in its presentation, but its ing both STATEMATE and UML statechart seman- interpretation is significantly different. The activity tics. Other works use Petri-nets and their extensions diagram is essentially composed of activities and tran- (Colored Petri-nets, High-level Petri-nets) to formal- sitions. An activity specifies a behavior described by ize activity diagrams such as in [SH05, Sto04a, Sto05, an organized sequencing of units whose basic elements Sto04b, BG03]. are actions. The most common types of actions are: There is also some works use pi-calculus as seman- call operation, call behavior, send, accept event, accept tic domain to give formal semantics to activity dia- call, reply, create, destroy, and raise exception. Each grams such as in [Lam08] where the authors aim to of them is used to represent the adequate behavior. A check a model against its specifications expressed in transition materializes the transition from one activ- modal mu-calculus, and also in [YZ04], where a full ity to another, it is triggered when the source activity formal framework is proposed using pi-calculus. The is completed and immediately causes the start of the automation of the translations is not provided. target activity. Therefore, transitions allow specifying To build automation translations, some works sequence of treatments and define the control flow. Ac- adopted CASE tools such as AToM3 tool which has tivity diagrams provide the mechanism for partitions, been used with success in those projects. In [GD03], called swimlanes which allow organizing the nodes of an AToM3 integrated framework has been developed activities by making regroupings. for the verification of UML models using Petri Nets. They build meta-models for an UML design (composed 3.2 Pi-calculus of Class, Statecharts and Sequence diagrams) in addi- tion to a Petri Nets meta-model. Then, they use graph The pi-calculus [Mil99] is a formal language that has grammars to translate the former to the later which al- solid mathematical bases. It is a computing model International Conference on Advanced Aspects of Software Engineering Page 108 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 that is used to represent concurrent and mobile sys- 4 The framework tems by the expression of interactions between evolv- 4.1 Overview ing processes, its two basic concepts are Names and Processes. A Name represents channels(ports), vari- In our framework, a combined meta-modelling and ables, data while a Process represents a communicat- graph grammar approach is adopted to build an in- ing entity in a system. The syntax of the pi-calculus tegrated tool using the AToM3 (see Figure 1). The process expression is given in Table 1: approach consists of two essential tasks; firstly, we needed to propose a meta-model for activity diagrams to generate an AToM3 integrated environment which supports the visual modeling of these diagrams. Sec- ondly, we have proposed and developed a graph gram- mar which gives us for each activity diagram mod- eled in the tool its corresponding pi-calculus process expression. This last is uploaded immediately in the mobility workbench (MWB) [VM94] to start the ver- ification task. Thirdly, the results of the verification will be exported to the graph grammar (a feedback) that try to identify the problem found by interpreting Table 1: pi-calculus Process Expression these results and makes a sign on the diagram itself (the deadlock as example). 3.3 Graph Transformation and AToM3 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 Figure 1: The framework architecture syntax (the relationships between the elements) of any formalism, and its concrete syntax (the graphical no- tation that must be respected by models). Graph grammars [Roz97] are generalization of 4.2 Formalization of activity diagrams using Chomsky grammars for graphs. In AToM3, a graph pi-calculus grammar is composed of an initial action, multiple Activity diagrams must be provided with formal se- rules and a final action. Initial and final actions are mantics in order to be able to verify any aspect of used to provide necessary information before and after the behavior [Rod00]. To overcome this problem the the execution of the rules. Each rule has two graphs; pi-calculus can be used for the verification by a trans- one on its left called the LHS (Left Hand Side) and formation approach of the activity diagrams into pi- another one on its right called the RHS (Right Hand calculus (Table 2) Side). A rule is evaluated by comparing its LHS with a zone in an input graph (called host graph). If a 4.3 Activity diagram Meta-model matching is found, the rule will be executed and the corresponding matching sub-graph in the host graph Our meta-model is composed of 8 classes and 7 will be replaced by the rule RHS. Furthermore, a rule associations developed by the meta-formalism (CD- may also have a condition that must be satisfied to ap- classDiagramsV3) in order to have an AToM3-based ply the rule, as well as actions to be performed when tool which offers the necessary tools to model the ac- the rule is carried out. The tool has a rewriting sys- tivity diagrams (see Figure 2). tem that iterates applying the matching rules in the After we have come to model our meta-model, only graph grammar to the host graph, until no rule is ap- its generation remains. The generated meta-model plicable. The rules are also ordered in this tool by a contains the set of classes modeled as buttons that user-assigned priority (higher to lower). are ready to be used for a possible modeling of an ac- International Conference on Advanced Aspects of Software Engineering Page 109 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 Figure 2: Activity diagrams meta-model under AToM3 tivity diagram. The generated environment is shown in Figure 3: 4.4 The Graph grammar The construction of graph grammar rules is an impor- tant step in the process of implementing a graph trans- formation. 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 final 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. • Initial action: Table 2: Formalization of Activity Diagram Role: In the initial action of the graph grammar we have created a file with sequential access named ”pi- calculus.txt” to store the generated pi-calculus code. • Final action: International Conference on Advanced Aspects of Software Engineering Page 110 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 Figure 5: The rules initial2decision, initial2fork, ini- tial2merge Figure 3: Activity diagrams environment under AToM3 Name : Action2picalcul Priority : 2 Role: In the final action of the graph grammar, we Role:This rule allows transforming an Action with close the file ”picalculus.txt”. the incoming arc from an action and the outgoing arc that ends to an action, in this rule we return the name • Rules: of the action and the name of the incoming and out- going arc (see Figure 6). 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 file ”pical- culus.txt” and adds the class in the pi-calculus code (see Figure 4). Figure 6: Action mapping in the graph grammar Examples of similar rules are Action2decision, Ac- tion2Fork, Action2join, Action2merge, Action2final, ...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). Figure 4: Initial node mapping in the graph grammar An example of a similar rule is join2picalcul. It is applied to locate a join node, and transforms it to pi- Similar rules are initial2decision, initial2fork, ini- calculus code according to the semantic rules already tial2merge, they are described in Figure 5. The dif- described in Table 2. ference is in the code python used to generate the pi- Rule 5 : Merge mapping calculus code as already seen in table2. Name : merge2picalcul Rule 2 : Action mapping Priority : 3 International Conference on Advanced Aspects of Software Engineering Page 111 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 Figure 7: Fork mapping in the graph grammar Role:This rule transforms a merge node with two Figure 8: Merge mapping in the graph grammar 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 Example In order to concretize the usefulness of the defined graph transformation, we tried to apply it to the sim- ple example of the activity diagram presented in Fig- ure 9. It should be noted that this example does not Figure 9: Example of an activity diagram claim to be exhaustive, but it includes some important elements of an activity diagram such as: action, fork, join..etc. 6 Conclusion The generated pi-calculus code is described in Fig- The result of our work is an automatic approach that ure 10: enables visual modeling of systems behavior using If we remove the transition between the action ”del- UML activity diagrams and their verification using pi- liverorder” and the final node, we create a deadlock in calculus. The proposed approach is based on the graph the diagram. Thus, the reloaded pi-calculus code will transformation, and it is carried out using the AToM3 be similar except for the process (agent): tool. The meta-modeling is used to define an envi- agent delliverorder(x6,x7) = ronment for activity diagrams while the graph gram- x6.t.delliverorder(x6,x7) mars are used to automate the translation and the Our tool will analyze the code using MWB, it im- analysis feedback. We saw in the last example the mediatly detects the deadlock (a state that has no out- deadlock property, some other properties need more going transitions) and the process concerned. The final advanced feedback mechanisms to be understandable action of the graph grammar points out the problem such as counter-examples. In future work, we plan to by coloring the the corresponding element of the dead- enable such mechanism by interpreting feedback anal- locked process in the graph of the diagram (see Figure ysis using Sequence Diagrams depicted in AToM3. In 11). addition, we intend formalizing and integrating in our International Conference on Advanced Aspects of Software Engineering Page 112 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 8th International Conference, AMAST 2000, volume 1816 of LNCS, pages 293–308. Springer-Verlag, 2000. [Rod00] R. W. S. Rodrigues. Formalising UML Ac- tivity Diagrams using Finite State Processes, UML2000 workshop.2000. Figure 10: The generated pi-calculus code [BD00a] C. Bolton and J. Davies. On giving a behav- ioral 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 For- mal Methods, LNCS 1945, 2000, pp. 77-96. [EW02] R. Eshuis and R. Wieringa. Verification sup- port for workow design with UML activity graphs, in 22nd Int. Conf. on Software Engi- neering, ACM Press, 2002, pp. 166-176. Figure 11: The analysis feedback on the diagram [Esh06] R. Eshuis. Symbolic model checking of UML activity diagrams, ACM Trans. Software En- framework other notational elements such as expan- gineering and Methodology 15(1), 2006. sion region and interruptible activity region. We plan also to apply our approach to a wider range of real- [SH05] H. Storrle and J. H. Hausmann. Towards a world critical systems in order to experiment its per- formal semantics of UML 2.0 activities, in formance. German Software Engineering Conf. 2005, 2005. References [OMG17] Object Management Group (OMG). Unified [Sto04a] H. Storrle. Semantics of Control-Flow in Modeling Language (UML), Superstructure, UML 2.0 activities, in 2004 IEEE Symp. Vi- v2.5, http://www.omg.org/, 2017. sual Languages and Human Centric Comput- ing, IEEE Computer Society, pp. 235-242, [VM94] B. Victor, F. Moller. The Mobility Work- 2004. bench -A Tool for the pi-calculus. In: Dill, D. (ed.) CAV 1994. LNCS, vol. 818, pp. 428- [Sto05] H. Storrle. Semantics and verification of data 440. Springer, Heidelberg, 1994. flow in UML 2.0 activities, Electronic Notes in Theoretical Computer Science 127,35-52, [Roz97] G.Rozenberg. Handbook of Graph Gram- 2005. mars and Comp (Vol. 1). World scientific. doi:10.1142/3303, 1997. [Sto04b] H. Storrle. Structured nodes in UML 2.0 ac- tivities, Nordic Journal of Computing 11(3) [Mil99] R. Milner. Communicating and Mobile Sys- (2004) 279-302. tems: The pi-calculus. Cambridge University Press, 1999. [BG03] J. P. Barros and L. Gomes. Actions as activi- ties and activities as Petri nets, in Workshop [OMG04] Object Management Group (OMG), on Critical Systems Development with UML, Model Driven Architecture (MDA), 2003. http://www.omg.org/mda , 2004. [ATo02] AToM3 home page, (online) available at: [Lam08] V.S.W. Lam. On pi-calculus semantics as a http://atom3.cs.mcgill.ca/, 2002. formal basis for UML activity diagrams. In- ternational Journal of Software Engineering [BCR00] E. Borger, A. Cavarra, and E. Riccobene. An and Knowledge Engineering 18(4), 541-567, ASM Semantics for UML Activity Diagrams. 2008. International Conference on Advanced Aspects of Software Engineering Page 113 ICAASE, December, 01-02, 2018 A Graph Transformation of Activity Diagrams into Pi-calculus for Verification Purpose ICAASE'2018 [YZ04] D. Yang, S.S. Zhang. Using pi-calculus to for- malize UML activity diagrams. In: 10th Int. Conf. and Workshop on the Engineering of Computer-based Systems, pp. 47-54. IEEE Computer Society, 2004. [GD03] E. Guerra and J. DeLara. A Framework for the Verification of UML Models. Examples using Petri Nets. In JISBD’03. Alicante,2003. [Ker+10] E. Kerkouche, A. Chaoui, E. Bourennane, O. Labbani. A UML and Colored Petri Nets Integrated Modeling and Analysis Approach using Graph Transformation. In Journal of Object Technology, vol. 9, no. 4, 2010, pages 25-43. [CEC12] W. Chama, R. Elmansouri, A. Chaoui. Model Checking and Code Generation for UML Diagrams using Graph Transforma- tion. International Journal of Software En- gineering and Applications (IJSEA), Vol.3, No.6, November, 2012. [Bel+14] A. Belghiat, A. Chaoui, M. Maouche, M. Beldjehem. Formalization of Mobile UML Statechart Diagrams using the pi-calculus: An Approach for Modeling and Analysis. In G. Dregvaite and R. Damasevicius (Eds.): ICIST, CCIS 465, pp. 236247. Springer, 2014. [BC16] A. Belghiat, A. Chaoui. Mapping Mobile Statechart Diagrams to the Pi-Calculus us- ing Graph Transformation: An Approach for Modeling, Simulation and Verification of Mobile Agent-based Software Systems. Inter- national Journal of Intelligent Information Technologies (IJIIT) 12(4), 2016. [BCB16] A. Belghiat, A. Chaoui, and M. Beldje- hem.Capturing and Verifying Dynamic Sys- tems Behavior Using UML and Pi-Calculus. In Theoretical Information Reuse and Inte- gration (pp. 59-84). Springer, 2016. International Conference on Advanced Aspects of Software Engineering Page 114 ICAASE, December, 01-02, 2018