UML-VT: A Formal Verification Environment for UML Activity Diagrams Zamira Daw, John Mangino, and Rance Cleaveland Department of Computer Science, University of Maryland Abstract—This paper introduces a translation tool that sup- purpose of this integration is to provide formal verification in ports formal verification of UML activity diagrams using the the early phases of development regardless of ones knowledge model checkers: UPPAAL, SPIN, NuSMV and PES. The moti- of formal methods. Furthermore, the integration leverages the vation for this tool arises from the desire to check the properties of a system early in the development process, and the fact higher abstraction of the UML models in order to reduce the that UML is commonly used to describe software models. The state explosion problem, thereby allowing the verification of tool is implemented as an Eclipse-plugin that automatically more complex systems. translates the UML activities and logical requirements into valid The UML-VT transforms UML activities into the input input notation for the model checkers. The automated aspect notation for the model checkers: UPPAAL, SPIN, NuSMV of the plugin allows users without a background in formal methods to verify the safety and liveness of a system. The and PES. The used transformation strategies have been chosen translation strategies implemented in this plugin are the result based on the results of an experimental study conducted of an experimental study. A tutorial video can be found in by the authors [3]. This paper presents the capabilities and https://www.youtube.com/watch?v=AHsih8REUxM. functionality of the UML-VT as well as references for theo- I. I NTRODUCTION retical and technical work, on which this tool is based. The plugin and source code of the UML-VT can be found at A major concern in system development is the correctness http://www.cs.umd.edu/∼rance/projects/uml-vt/ of software components. The benefit of formal methods is that they verify the systems correctness against specific require- II. F UNCTIONALITY ments for all possible inputs. In contrast to testing, formal methods allow not only the verification of the presence of an The UML-VT is an open-source Eclipse plug-in that ver- error in a system, but also the verification of the absence of ifies UML activities against given requirements using well- errors. Automated formal verification such as model check- know model checker tools such UPPAAL [4], SPIN [5] and ing [1] has been improved in the last decades, allowing the NuSMV [6], and an experimental model checker PES [7]. verification of more complex software systems. However, the The inputs of the verification are the UML models and the usage of model checking is limited by the required knowledge requirements. The format of the UML models is *.uml, which of formal methods, as well as by the state explosion problem, can be exported from the majority of UML-Tools such as which restricts the size of systems that are verifiable. Papyrus1 or MagicDraw2 . Requirements have to be specified Model-driven development (MDD) has been used in soft- as a temporal logic formula, which can be created using a ware development in order to handle the development of Requirement Editor provided by the UML-VT. The output complex systems. In MDD approaches, designers first build of the verification is a report that shows the satisfiability of models of the desired software, which can be manually or the given requirement and counter examples that violate the automatically (code generation) transformed into develop- requirement (depending of the chosen model checker). ment artifacts (e.g. source code). The models abstract ele- The UML-VT also provides an Eclipse Perspective shown ments/behaviors of the systems, thereby reducing the com- in Figure 1 in order to facilitate the verification workflow. The plexity of the development and facilitating the understanding Perspective can be open by the following menu chain: Window of the system. Unified Modeling Language (UML) [2] has → Open Perspective → Other → UML-VT. The perspective attracted substantial attention as a language for MDD. More- contains four views and one menu. View 1 shows the Project over, UML is a non-proprietary, independently maintained Explorer, View 2 is reserved for the chosen modeling tool, standard, which provides several graphical sublanguages and View 3 shows the Console which will update the user on an extension mechanism (profiling). A UML activity diagram the current state of the verification process, and View 4 is a behavioral diagram that is generally used to specify the displays the report file, which contains the results of the model workflow of a system. The presented tool uses UML activity checker. The UML-VT Menu allows the user to start the diagrams in order to specify the behavior of the system. verification (Verify), to set the paths of the model checkers The UML Verification Tool (UML-VT) is meant to support executable file (Configuration), and to set a default model the integration of model checking into a MDD process. The 1 https://eclipse.org/papyrus/ Research supported by NSF Grant CCF-0926194 2 http://www.nomagic.com/products/magicdraw.html checker (Model checkers). This menu is only displayed if the ment Editor. The editor aims to facilitate the specification UML-VT Perspective is active. of temporal logic formulas by highlighting keywords and checking syntax. LTL and CTL formulas are supported. The editor syntax is model checker independent. An example requirement for the activity in Figure 3 can be ”In all execution paths, the ActionB should be executed at least one time”. The temporal logic formula corresponding to the requirement is: AF Activity2 :: ActionB (1) AF Activity1 :: Action2 :: ActionB (2) Note that equation 1 verifies the ActionB if the main activ- ity would be Activity2 and equation 1 verifies the same action but if the main activity would be Activity1. Requirement Editor provides code completions, which suggests a list of possible names of actions. Fig. 1. Eclipse-Plugin of the UML-VT The verification workflow is shown in Figure 2. Create project: A new project can be created using File → New → Project → UML-VT → Project. The created project contains by default a Papyrus model, DMOSES Profile [8], and the Requirement file. The DMOSES Profile is explained in the modeling section. Fig. 3. UML activity example Generation of model-checker specific properties: Once the Requirements.tl file is saved, model-checker specific formulas are generated in the scr-gen folder according to the chosen model checker. Formulas that are not supported by the given model checker (e.g. UPPAAL only allows only a subset of CTL∗ [9]) are not transformed into model-checker specific formulas and are shown in the console. Translation from UML-models into model-checker lan- guages: The translation is started by clicking the Verify button in the UML-VT Menu. Depending on the chosen model checker a different translation is executed. The translations support hierarchical modeling and also apply optimization techniques. The generated files are saved in the scr-gen folder. Fig. 2. Workflow of the UML-VT These files are the input for the model checkers. Modeling: The user can model the system within the Papyrus model or using his/her preferred UML-Tool. However, note that the verification requires the file *.uml. If MagicDraw is used as modeling tool, this file can be obtained by File → Export To → Eclipse UML2. The DMOSES profile is a UML profile that extends UML activity diagrams and state machine Fig. 4. Possible main activities to verify diagrams in order to add information regarding execution time, parallelism and priority [8]. This profile gives an unambiguous Model checking execution: After a successful translation, behavior specification, which is required for the formal veri- a window pops up with a list of all possible main activities fication. An example of an extended UML activity is shown as shown in Figure 4. Thus, the user can select the main in Figure 3. activity of the system, afterwards the chosen model checker Requirements specification: The user can specify the re- is automatically invoked. There is a timeout that limits the quirements with in the file Requirements.tl using the Require- verification time. Display of verification results: The results of the verifica- graph by merging sequential vertices and normalizes execution tion are saved in the report.txt file and are displayed after times. These transformations are implemented using an eclipse the model checker has finished. Current efforts address a plug-in called ATL (ATLAS Transformation Language)3 . model checker independent report in order to facilitate the understanding of the results. Figure 5 shows the verification result of the example in Figure 3 and the requirement of formula 2. Note that the property is not satisfied, which implies that the action is not executed. This is because the event e1 is sent only after it is received. Since there are no other activities that send this event, actions within Figure 3 are never executed. Errors such as this one are not easy to find in a model with multiple activities and multiple hierarchical levels. This example shows how the correctness of the model can be easily verified using the UML-VT. Fig. 5. Verification results of Formula 2 using UPPAAL III. A RCHITECTURE Fig. 7. Workflow transformation from UML models into model-checker input notation The UML-VT Eclipse-plugin can be divided into four main components: Model Transformation, Code Generation, The Code Generation module is based on templates that a Requirement Editor, and a User Interface as is shown in specify the behavior of the different elements of the UML Figure 6. The User Interface aims to facilitate the interaction activities using the model-checker languages. For example, with the user by providing a Perspective, Menus, Project for UPPAAL, the template UPPAAL Tp specifies the token- Wizards, Plugin-Installation, Verification Management, etc. based behavior of the UML activities using Timed Automata. This component is primary based on the Rich Client Platform Note that the templates encompass sophisticated understanding (RCP) provided by Eclipse. formal-methods. Since there are multiple ways to specify this behavior using model-checker languages, the authors conducted an experimental study to analyze the influence of different translations strategies on the verification perfor- mance [3]. The templates that are used correspond to the best translation strategies for each model-checker in relation to the results of the study. Code Generation module uses the plug-in Fig. 6. Architecture of the Eclipse-Plugin. Developed components (green) Xpand4 . The multiple intermediate steps between the UML are based on Eclipse components (blue), and external plugins (orange). models and the model-checker input notation are transparent for the user, who only sees the generated files for the model Due to space limitation, technical details of the translations checkers. can be found in [3]. The transformation of UML models into The correctness and scalability of the transformations, opti- model-checker input notation is implemented in two modules: mizations and code generation have been tested using a bench- Model Transformation and Code Generation. The interaction mark composed of a set of 67 UML activity diagrams and a between these parts is shown in Figure 7. Note that an interme- model of a medical device case study, an infusion pump [3]. diate graph is used. Thus, UML models are transformed into The UPPAAL translation achieves the best performance in the graphs by the Model Transformation module, and afterwards, verification of UML activities, in particular for big models, graphs are transformed into model-checker input notation since the variable management of this model checker in the by the Code Generation module. The intermediate graph creation of the state space of the system. is used in order to facilitate the transformation of multiple The plug-in Xtext5 is used in the component Requirement diagrams, the generation of multiple model-checker languages, Editor. The component specifies the domain-specific language and the implementation of optimization algorithms. The Model of the temporal logic formulas, and implements the editor and Transformation module consists of three components: Model the generation of the model-checker specific formula files. to Model Transformation, which transforms UML models into graphs, Hierarchy Management, which flattens multiple hier- 3 https://eclipse.org/atl/ archical levels (e.g. modeled by using CallBehaviorActions), 4 http://wiki.eclipse.org/Xpand and Optimization, which reduces the number of vertices of the 5 https://eclipse.org/Xtext/ IV. R ELATED W ORK tool allows the verification of models with an EMF input To the best of our knowledge, there is an apparent lack of format, which can be exported from the majority of UML- tools aimed at formal verification of UML activities. Although Tools. The UML-VT supports the verification using the model there are different approaches that propose the verification of checkers UPPAAL, SPIN, NuSMV, and PES. The support of UML activities using model checking, summarized in [3], the multiple model checkers allows the user to choose the most majority of these approaches do not provide a public tool appropriate model checker with respect to the target platform. (or it could not be found). Similar to the presented tool, Generation of model-checker input notation is based on model- these approaches use translational strategies to generate model- to-model transformations, which optimize the space state of checker languages. In general, these approaches offer only the system, and on templates, which encompass the knowledge the usage of one model checker. In contrast, the UML-VT of a model-checking expert. These templates are also tied to supports four model checkers, and provides an open-source our interpretation of the UML models, which is based on Eclipse plugin. the DMOSES profile. This limitation can be overcome by MADES project propose a tool chain [10] to verify UML extending the transformations in order to support other UML Model of embedded systems. MADES uses its own model profiles or other diagrams. checker. In [11], dos Santos also presents a formal verification In our ongoing work, we address this limitation in a more tool for UML behavioral diagrams using NuSMV. Similar general way by allowing the user to specify its own formal to our approach, these tools presents translations from UML semantics by using an extensible formal semantics [12]. The model into the model-checker input notation. In contrast to extensible semantics provides a reference semantics that can be UML-VT, these tools force the user to use only one model extended according to the interpretation of the UML models. checker. Furthermore, the translations provided by the UML- A label transition system (LTS) is generated from the input VT are based on an experimental study providing a higher UML models according to the user-specific semantics. The confiability. It is worth mentioning that these tools where not LTS formally specifies the behavior of the system. We are available to download, and therefore the description is based working in a semantics framework tool that allows specifying only on academic publications. the extensible semantics, and provides simulation of the UML models, consistency verification of the semantics (bisimula- V. D ISCUSSION tion) and formal verification (translation from LTS into model- The usage of UML models as an input notation of the ver- checker input notation) based on the user-specific semantics. ification has three main advantages. 1) It is easier to integrate R EFERENCES the verification in the MDD process because these models are [1] C. Baier, J.-P. Katoen et al., Principles of model checking. MIT press also used during the development process. 2) The abstraction Cambridge, 2008, vol. 26202649. of the UML models mitigates the state-explosion problem [2] OMG, Unified Modeling Language, Superstructure, Version 2.4.1, of the model-checking algorithm. Furthermore, the DMOSES http://www.omg.org/spec/UML/2.4.1/Superstructure/PDF, 2011. [3] Z. Daw and R. Cleaveland, “Comparing model checkers for timed uml profile adds additional information about the implementation activity diagrams,” Science of Computer Programming, 2015. (e.g. execution time) that allows verifying the system taking [4] G. Behrmann, A. David, and K. Larsen, A Tutorial on Uppaal. into account implementation features. The DMOSES profiles Springer Berlin Heidelberg, 2004, vol. 3185, pp. 200–236. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-30080-9 7 also contributes to the reduction of the state-space since this [5] G. J. Holzmann, “The model checker spin,” IEEE Transactions on UML extension provides a deterministic behavior and reduces Software Engineering, vol. 23, no. 5, pp. 279–295, 1997. the behavior concurrency by giving a limited processing units. [6] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, NuSMV 2: An These aspects allow the application of model checking without OpenSource Tool for Symbolic Model Checking. Springer Berlin any further optimization methods (e.g. CEGAR). 3) Since Heidelberg, 2002, vol. 2404, pp. 359–364. [Online]. Available: UML models are model-checker independent, model-checker http://dx.doi.org/10.1007/3-540-45657-0 29 [7] D. Zhang and R. Cleaveland, “Fast on-the-fly parametric real-time model specific translations can be implemented, which facilitate the checking,” in Real-Time Systems Symposium, 2005. RTSS 2005. 26th choice of the model checker. Although the choice of a model IEEE International, Dec 2005, pp. 10 pp.–166. checker should primarily depend on its ability to address the [8] Z. Daw and M. Vetter, Deterministic UML Models for Interconnected Activities and State Machines. Springer Berlin Heidelberg, 2009, vol. system domain or the properties to verify, in practice, the 5795, pp. 556–570. model checker is chosen based on the previous experience [9] A. Pnueli, “The temporal logic of programs,” in Foundations of Com- of the formal method experts. Thus, the support of multiple puter Science, 18th Annual Symposium on. IEEE, 1977, pp. 46–57. [10] A. Radjenovic, N. Matragkas, R. F. Paige, M. Rossi, A. Motta, L. Baresi, model checkers by the UML-VT allows users to use the most and D. S. Kolovos, “Mades: a tool chain for automated verification adequate model checker for the application area (e.g. UPPAAL of uml models of embedded systems,” in Modelling Foundations and for real-time systems or SPIN for distributed systems). Applications. Springer, 2012, pp. 340–351. [11] L. B. R. dos Santos, E. R. Eras, V. A. de Santiago Júnior, and N. L. VI. C ONCLUSION AND F UTURE W ORKS Vijaykumar, “A formal verification tool for uml behavioral diagrams,” in Computational Science and Its Applications–ICCSA 2014. Springer, The UML-VT enables formal verification of UML activities 2014, pp. 696–711. using model checkers. The tool is implemented in Eclipse, [12] Z. Daw and R. Cleaveland, “An extensible operational semantics for uml activity diagrams,” in International Conference on Software Engineering which is already known as a modeling and MDD environment. and Formal Methods, 2015. In order to facilitate the integration to any MDD process, the