=Paper=
{{Paper
|id=Vol-1848/CAiSE2017_Forum_Paper12
|storemode=property
|title=Regression Testing for Visual Models
|pdfUrl=https://ceur-ws.org/Vol-1848/CAiSE2017_Forum_Paper12.pdf
|volume=Vol-1848
|authors=Ralf Laue,Arian Storch,Markus Schnädelbach
|dblpUrl=https://dblp.org/rec/conf/caise/0001SS17
}}
==Regression Testing for Visual Models==
https://ceur-ws.org/Vol-1848/CAiSE2017_Forum_Paper12.pdf
Regression Testing for Visual Models
Ralf Laue1 , Arian Storch2 , and Markus Schnädelbach3
1
University of Applied Sciences Zwickau, Department of Computer Science
Dr.-Friedrichs-Ring 2a, 08056 Zwickau, Germany
ralf.laue@fh-zwickau.de
2
it factum GmbH, Arnulfstr. 37, 80636 Munich, Germany
arian.storch@bflow.org
3
Saxon Police Force - Computer and Internet Crime Unit, Germany
Abstract. In this paper, we present a set of Eclipse plug-ins which
adapts the idea of regression testing for the area of visual modelling in
software engineering: Expected properties of models in languages such
as UML, BPMN, etc. are stored together with the model (comparable
with test cases added to software). With each change of the model, these
properties can be checked. The solution should work with any visual
modelling language included into Eclipse – both for standardised as for
domain-specific languages.
The advantage of our approach over current existing solutions is that
the process of model checking is completely hidden to the modeller. In
particular, it is not necessary for the modeller to learn a formalism for
specifying expected properties.
1 Introduction
In this paper, we present a set of Eclipse plug-ins that aim to improve the
quality of visual models in languages such as UML, SysML or BPMN, but also in
domain-specific visual languages. For this purpose, the idea of regression testing
which is a well-known paradigm in software engineering is adapted for the domain
of visual modelling. In software engineering, regression testing makes sure that
software still works correctly after it has been changed. This avoids that desirable
properties (expressed as test cases) get lost with a software change. It is good
practice to run such tests after each software change. If the results for all test case
executions are “green” (Fig. 1), the software developer knows that the software
still has the behaviour which is expected by the test cases.
We would like to achieve the same for the domain of visual models in software
engineering: Expected properties are stored together with the models and can
be tested with every change of the model. However, here we face a different
situation: While a typical software developer is able to write test cases (which
are executable computer programs as well), we cannot expect that every modeller
can formulate desirable model properties in a formal language that is needed for
model verification. In [1], Visser et al. point out that hiding the formal models
and specification formalisms from the end-user is paramount to the success of
X. Franch, J. Ralyté, R. Matulevičius, C. Salinesi, and R. Wieringa (Eds.):
CAiSE 2017 Forum and Doctoral Consortium Papers, pp. 89-95, 2017.
Copyright 2017 for this paper by its authors. Copying permitted for private and academic purposes.
Fig. 1. “All tests green” in JUnit
formal verification. With our Eclipse plug-ins, we provide the possibility to hide
both the formal model that is needed by the model checker as the formalism
needed for specifying properties. This enables end users who are not experts for
formal methods to use the “regression testing” feature for visual models.
2 Challenges of “Hiding” Formal Methods
The usual way for verifying properties of visual models in software engineering
starts with transforming the model into another (formal) model that can be
analysed by a verification tool. This formal model can be e.g. a Petri net or
an abstract automaton that can be processed by a model checker. In the most
cases, the verification tool (a model checker, a SAT solver, a natural language
processing tool, etc.) already exists independently from the modelling tool. If
we want to use such a tool for “regression testing” of visual models, we face the
following challenges (cf. [1]):
1. The visual model has to be transformed into the formal language the tool
can work with.
2. The properties to be verified have to be transformed into a formal language
understood by the tool.
3. Starting the verification tool should be possible directly from the modelling
tool’s user interface.
4. The information which of the checked properties are fulfilled should be shown
in the modelling tool’s user interface.
5. If a property is not fulfilled, an explanation of the reasons (such as a coun-
terexample found by a model checker) should be transferred back to the
visual model.
6. The tested properties have to be bound to the model such that they can be
checked again with the next change of the model.
Our set of Eclipse plug-ins, called the bflow* Hive, provides a solution to those
challenges. Originally the plug-ins have been developed for the bflow* Toolbox
[2], an Eclipse-based open-source tool for business process modelling with Event-
Driven Process Chains. Now, the current version of our Eclipse plug-ins should
work with every graphical modelling tool that is based on Eclipse using GMF
or Graphiti.
The basic steps for integrating model verification into the user interface of a
modelling tool (model transformation into a formal language, starting external
verification tool and visualising its results in the modelling tool) are described
90
Fig. 2. Property Specification with Temporal Logic (example taken from [4])
(a) source: [5] (b) source: [6] (c) source: [7]
Fig. 3. Property Specification with Visual Languages
in [3]. Here, we would like to discuss a recent enhancement that deals with point
(2) from the above list – a point which is often neglected by current tools. For
our discussion, we use examples from the area of business process modelling.
However, we want to emphasise that our solution is independent from modelling
languages and application domains.
Point (2) from the above list - specifying the properties to test - is not yet
satisfactory implemented by several current tools that verify properties of visual
models. In the area of business process modelling and compliance checking, we
often encounter the need to specify the properties as temporal logic formulae
(see Fig. 2) or as OCL constraints.
Other authors suggested graphical languages for specifying the expected
properties; some examples are shown in Fig. 3. The disadvantage is that mod-
ellers have to learn one more visual language.
Our approach for specifying properties is to use patterns for frequently oc-
curring model properties. This idea goes back to the work of Dwyer et al. [8] who
developed a set of property specification patterns such as “Response” (A must
always be followed by B) or “Absence” (A must never happen). In the spirit
of this work, specific property specification patterns for business processes have
been developed [9, 10]. In [10], the participants of a study were able to express
72 out of 82 business compliance rules by means of these patterns.
Wong and Gibbons [11] showed how Dwyer’s patterns can be used for verify-
ing properties of BPMN models. This means that the theory of using specification
patterns for verifying properties of business process models is well-researched.
However - to the best of our knowledge - this method was rarely included into
publicly available modelling tools. Notable exceptions are [9] as one of the first
works on applying patterns for property verification and the work by the groups
who have developed the specification patterns (see e.g. [12] and [10]).
91
Fig. 4. Selecting the Properties to Verify from a List of Property Patterns
3 Example
Business process models often have to adhere to certain compliance rules such
as “After each customer request we receive, an offer will be sent”. To ensure a
high quality of the model or the adherence to compliance rules, it is desirable
to verify such properties after each change of the model. Using the terminology
from [8], the mentioned property can be described by the specification pattern
“Response”. A modeller who wants to verify this property in our tool bflow*
Toolbox opens the Eclipse view “Model properties” (which is provided by our
plug-ins) and selects the appropriate pattern from a menu as shown in Fig. 4.
Next, the placeholders in the property specification are bound to shapes in the
diagram (i.e. to tasks in the depicted business process) by firstly clicking on
the hyperlink for the placeholder and secondly clicking on the shape. When all
properties are bound to concrete model elements, both the model to be verified
as its expected properties are transformed into the input language of a formal
tool. For demonstrating the approach, we transform a business process model
in the language Event-Driven Process Chains into a network of automata that
can be verified by the model checker UPPAAL. In addition, the properties to be
verified are translated into a temporal logic formula as well. For this purpose,
a template has to be provided which lists the property specification patterns
as well as their formal representation in the language of the model checker.
Of course, an expert in formal methods is needed for creating these templates.
92
However, once the templates exist, end-users can use them without any deeper
knowledge in this area. For example, for the mentioned property, this template
looks like this:
After execution of $function_1 , $function_2 will always be
executed later >>>i_$function_1.working-->i_$function_2.working
Next, the tool for verification (in our case, the model checker UPPAAL) is
called, its results are analysed and shown in the Model Properties view in the
same way. The properties are marked as “red” or “green” (see Fig. 5) in the
same way as in Eclipse’s JUnit plug-in (Fig. 1).
Fig. 5. The Results of the Analysis are Shown as “Red” or “Green”
4 Using our Plug-ins in Eclipse-Based Modelling Tools
While the example in the previous section deals with business process models,
the pattern-based approach can be used for other types of modelling as well. For
example, property specification patterns have been used for verifying properties
of UML state charts [13, 14] or goal models [15]. [16] discusses the development
for property specification patterns for arbitrary domain-specific languages. To
sum up, we believe that the bflow* Hive can be useful for a great variety of
different types of modelling, including domain-specific approaches. To give an
example, Fig. 6 shows how our plug-ins have been used for verifying typical
properties of models in the goal-oriented modelling language ı̇∗ .
93
Fig. 6. Property Verification in an ı̇∗ Model
Our collection of plug-ins, called the bflow* Hive, is already integrated into
our own EPC modelling tool bflow* Toolbox 1 and into UPROM [17] (a mod-
elling tool that allows functional software size estimation) and (partly) in the ı̇∗
modelling tool openOME 2 .
As already mentioned, modelling tool developers can include the functionality
described in this article into their own Eclipse-based modelling tool just by
adding our plug-ins to the tool.
Compiled binaries and the source code can be obtained from the repository-
https://github.com/bflowtoolbox/ where all plug-ins named org.bflow.toolbox.
hive.* are part of the tool-independent bflow* Hive. The easiest way for a user to
profit from the features provided by the bflow* Hive in the modelling language
of his or her choice is to download the most recent version of the bflow* Toolbox
from the web site mentioned above and to use Eclipse’s update mechanism for
adding support for other modelling languages.
We are looking forward to reports from people who made use of the regression
testing feature or other bflow* Hive features into their tools.
Any questions related to our plug-ins are welcome to bflow@bflow.org.
References
1. Visser, W., Dwyer, M.B., Whalen, M.W.: The hidden models of model checking.
Software and System Modeling 11 (2012) 541–555
2. Böhme, C., Hartmann, J., Kern, H., Kühne, S., Laue, R., Nüttgens, M., Rump,
F.J., Storch, A.: bflow* Toolbox - an open-source business process modelling tool.
In: Proceedings of the Business Process Management 2010 Demonstration Track.
(2010) 46–51
3. Laue, R., Storch, A., Höß, F.: The bflow* Hive - adding functionality to Eclipse-
based modelling tools. In: Proceedings of the BPM Demo Session 2015. (2015)
120–124
4. Giordano, L., Martelli, A., Spiotta, M., Dupre, D.T.: Business processes verifica-
tion with temporal answer set programming. In: Proceedings of the 1st Interna-
tional Workshop on Knowledge-intensive Business Processes. Volume 861 of CEUR
Workshop Proceedings. (2012) 48–59
5. Forster, A., Engels, G., Schattkowsky, T., Van Der Straeten, R.: Verification
of business process quality constraints based on visual process patterns. Joint
IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (2007)
197–208
1
http://bflow.org
2
http://sourceforge.net/projects/openome/
94
6. Speck, A., Feja, S., Witt, S., Pulvermüller, E., Schulz, M.: Formalizing business
process specifications. Comput. Sci. Inf. Syst. 8 (2011) 427–446
7. Müller, J.: Strukturbasierte Verifikation von BPMN-Modellen. Vieweg+Teubner,
Wiesbaden (2011)
8. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for
finite-state verification. In: Proceedings of the second workshop on Formal methods
in software practice, ACM Press (1998) 7–15
9. Janssen, W., Mateescu, R., Mauw, S., Fennema, P., van der Stappen, P.: Model
checking for managers. In: 5th and 6th International SPIN Workshops. (1999)
92–107
10. Elgammal, A., Türetken, O., van den Heuvel, W., Papazoglou, M.P.: Formalizing
and appling compliance patterns for business process compliance. Software and
System Modeling 15 (2016) 119–146
11. Wong, P.Y., Gibbons, J.: Property specifications for workflow modelling. Science of
Computer Programming 76 (2011) 942 – 967 Integrated Formal Methods (iFM09).
12. Clarke, L.A., Avrunin, G.S., Osterweil, L.J.: Using software engineering technology
to improve the quality of medical processes. In: 30th International Conference on
Software Engineering (ICSE 2008), Companion Volume, ACM (2008) 889–898
13. Lopez, K., Cheng, B.H., Konrad, S., Goldsby, H.: Visualizing requirements in UML
models. First International Workshop on Requirements Engineering Visualization)
(2006)
14. Leitner-Fischer, F., Leue, S.: Quantum: Quantitative safety analysis of UML mod-
els. In: Proceedings Ninth Workshop on Quantitative Aspects of Programming
Languages. Volume 57 of EPTCS. (2011) 16–30
15. Van Lamsweerde, A.: Elaborating security requirements by construction of in-
tentional anti-models. In: Proceedings of the 26th International Conference on
Software Engineering, IEEE Computer Society (2004) 148–157
16. Meyers, B., Deshayes, R., Lucio, L., Syriani, E., Vangheluwe, H., Wimmer, M.:
ProMoBox: A framework for generating domain-specific property languages. In:
Software Language Engineering - 7th International Conference. Volume 8706 of
LNCS., Springer (2014) 1–20
17. Aysolmaz, B., Demirörs, O.: Automated functional size estimation using business
process models with UPROM method. In: 2014 Joint Conference of the Interna-
tional Workshop on Software Measurement and the International Conference on
Software Process and Product Measurement. (2014) 114–124
95
96