-This paper introduces a translation tool that supports formal verification of UML activity diagrams using the model checkers: UPPAAL, SPIN, NuSMV and PES. The motivation for this tool arises from the desire to check the properties of a system early in the development process, and the fact that UML is commonly used to describe software models. The tool is implemented as an Eclipse-plugin that automatically translates the UML activities and logical requirements into valid input notation for the model checkers. The automated aspect of the plugin allows users without a background in formal methods to verify the safety and liveness of a system. The translation strategies implemented in this plugin are the result of an experimental study. A tutorial video can be found in https://www.youtube.com/watch?v=AHsih8REUxM.
A major concern in system development is the correctness
of software components. The benefit of formal methods is that
they verify the systems correctness against specific
requirements for all possible inputs. In contrast to testing, formal
methods allow not only the verification of the presence of an
error in a system, but also the verification of the absence of
errors. Automated formal verification such as model
checking [
Model-driven development (MDD) has been used in
software development in order to handle the development of
complex systems. In MDD approaches, designers first build
models of the desired software, which can be manually or
automatically (code generation) transformed into
development artifacts (e.g. source code). The models abstract
elements/behaviors of the systems, thereby reducing the
complexity of the development and facilitating the understanding
of the system. Unified Modeling Language (UML) [
The UML Verification Tool (UML-VT) is meant to support the integration of model checking into a MDD process. The purpose of this integration is to provide formal verification in the early phases of development regardless of ones knowledge of formal methods. Furthermore, the integration leverages the higher abstraction of the UML models in order to reduce the state explosion problem, thereby allowing the verification of more complex systems.
The UML-VT transforms UML activities into the input
notation for the model checkers: UPPAAL, SPIN, NuSMV
and PES. The used transformation strategies have been chosen
based on the results of an experimental study conducted
by the authors [
The UML-VT is an open-source Eclipse plug-in that
verifies UML activities against given requirements using
wellknow model checker tools such UPPAAL [
The UML-VT also provides an Eclipse Perspective shown in Figure 1 in order to facilitate the verification workflow. The Perspective can be open by the following menu chain: Window ! Open Perspective ! Other ! UML-VT. The perspective contains four views and one menu. View 1 shows the Project Explorer, View 2 is reserved for the chosen modeling tool, View 3 shows the Console which will update the user on the current state of the verification process, and View 4 displays the report file, which contains the results of the model checker. The UML-VT Menu allows the user to start the verification (Verify), to set the paths of the model checkers executable file (Configuration), and to set a default model 1https://eclipse.org/papyrus/ 2http://www.nomagic.com/products/magicdraw.html checker (Model checkers). This menu is only displayed if the UML-VT Perspective is active.
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 [
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
diagrams in order to add information regarding execution time,
parallelism and priority [
Requirements specification: The user can specify the requirements with in the file Requirements.tl using the Requirement Editor. The editor aims to facilitate the specification 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:
(1) (2)
Note that equation 1 verifies the ActionB if the main activity 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.
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 [
Translation from UML-models into model-checker languages: 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. These files are the input for the model checkers.
Model checking execution: After a successful translation, a window pops up with a list of all possible main activities as shown in Figure 4. Thus, the user can select the main activity of the system, afterwards the chosen model checker is automatically invoked. There is a timeout that limits the verification time.
Display of verification results: The results of the verification are saved in the report.txt file and are displayed after the model checker has finished. Current efforts address a 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.
The UML-VT Eclipse-plugin can be divided into four main components: Model Transformation, Code Generation, a Requirement Editor, and a User Interface as is shown in Figure 6. The User Interface aims to facilitate the interaction with the user by providing a Perspective, Menus, Project Wizards, Plugin-Installation, Verification Management, etc. This component is primary based on the Rich Client Platform (RCP) provided by Eclipse.
Due to space limitation, technical details of the translations
can be found in [
The Code Generation module is based on templates that
specify the behavior of the different elements of the UML
activities using the model-checker languages. For example,
for UPPAAL, the template UPPAAL Tp specifies the
tokenbased behavior of the UML activities using Timed Automata.
Note that the templates encompass sophisticated understanding
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
performance [
The correctness and scalability of the transformations,
optimizations and code generation have been tested using a
benchmark composed of a set of 67 UML activity diagrams and a
model of a medical device case study, an infusion pump [
The plug-in Xtext5 is used in the component Requirement Editor. The component specifies the domain-specific language of the temporal logic formulas, and implements the editor and the generation of the model-checker specific formula files. 3https://eclipse.org/atl/ 4http://wiki.eclipse.org/Xpand 5https://eclipse.org/Xtext/
IV. RELATED WORK
To the best of our knowledge, there is an apparent lack of
tools aimed at formal verification of UML activities. Although
there are different approaches that propose the verification of
UML activities using model checking, summarized in [
MADES project propose a tool chain [
The usage of UML models as an input notation of the verification has three main advantages. 1) It is easier to integrate the verification in the MDD process because these models are also used during the development process. 2) The abstraction of the UML models mitigates the state-explosion problem of the model-checking algorithm. Furthermore, the DMOSES profile adds additional information about the implementation (e.g. execution time) that allows verifying the system taking into account implementation features. The DMOSES profiles also contributes to the reduction of the state-space since this UML extension provides a deterministic behavior and reduces the behavior concurrency by giving a limited processing units. These aspects allow the application of model checking without any further optimization methods (e.g. CEGAR). 3) Since UML models are model-checker independent, model-checker specific translations can be implemented, which facilitate the choice of the model checker. Although the choice of a model checker should primarily depend on its ability to address the system domain or the properties to verify, in practice, the model checker is chosen based on the previous experience of the formal method experts. Thus, the support of multiple model checkers by the UML-VT allows users to use the most adequate model checker for the application area (e.g. UPPAAL for real-time systems or SPIN for distributed systems).
The UML-VT enables formal verification of UML activities using model checkers. The tool is implemented in Eclipse, which is already known as a modeling and MDD environment. In order to facilitate the integration to any MDD process, the tool allows the verification of models with an EMF input format, which can be exported from the majority of UMLTools. The UML-VT supports the verification using the model checkers UPPAAL, SPIN, NuSMV, and PES. The support of multiple model checkers allows the user to choose the most appropriate model checker with respect to the target platform. Generation of model-checker input notation is based on modelto-model transformations, which optimize the space state of the system, and on templates, which encompass the knowledge of a model-checking expert. These templates are also tied to our interpretation of the UML models, which is based on the DMOSES profile. This limitation can be overcome by extending the transformations in order to support other UML profiles or other diagrams.
In our ongoing work, we address this limitation in a more
general way by allowing the user to specify its own formal
semantics by using an extensible formal semantics [