=Paper=
{{Paper
|id=Vol-1554/PD_MoDELS_2015_paper_16
|storemode=property
|title=UML-VT: A Formal Verification Environment for UML Activity Diagrams
|pdfUrl=https://ceur-ws.org/Vol-1554/PD_MoDELS_2015_paper_16.pdf
|volume=Vol-1554
|authors=Zamira Daw,John Mangino,Rance Cleaveland
|dblpUrl=https://dblp.org/rec/conf/models/DawMC15
}}
==UML-VT: A Formal Verification Environment for UML Activity Diagrams==
https://ceur-ws.org/Vol-1554/PD_MoDELS_2015_paper_16.pdf
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