Domain-specific modelling (DSM) helps designing systems at a higher level of abstraction, by providing languages that are closer to the problem space than to the solution space. Unfortunately, specifying and verifying properties of the modelled system has been mostly neglected by DSM approaches. At best, this is only partially supported by translating models to formal representations on which properties are specified and evaluated based on logic-based formalisms. This contradicts the DSM philosophy as domain experts are usually not familiar with such formalisms. To overcome this shortcoming, the ProMoBox approach lifts property specification and verification tasks up to the domain-specific level. For a given DSM language, some operations at the metamodel level are needed to allow specification and verification of properties. This paper reports on a practical case study of how to apply the ProMoBox approach on GISMO, a DSM language designed specifically for developing gestural interaction applications.
Domain-specific modelling (DSM) helps designing systems at a higher level of
abstraction. By providing languages that are closer to the problem domain than to the solution
domain, low-level technical details can be hidden. An essential activity in DSM is the
specification and verification of properties to increase the quality of the designed
systems [
In previous work we proposed the ProMoBox framework to shift property
specification and verification tasks up to the DSM level. The scope, assumptions and limitations
of this approach are presented in [
This paper presents a case study that applies ProMoBox to GISMO, a DSML for executable modelling of gestural interaction applications. We illustrate how to make some minor changes and additions to the metamodel of the DSML in order to enable the generation of all needed languages (an input language, output language, property language, and runtime language) that are required for the specification and verification of properties at DSM level. We subsequently report on the results of verifying these properties.
The paper is structured as follows. Section 2 presents the GISMO DSML used as a case study. Section 3 explains the changes required to the GISMO metamodel in order to apply the ProMoBox approach. Section 4 presents the results of applying ProMoBox to GISMO. Section 5 exemplifies the specification of domain-specific properties on GISMO models and provides some results and counter-examples found after verification of these properties. Section 6 presents related work, and Section 7 concludes. 2
GISMO is a DSML developed by the first author to facilitate development of
gesturebased interactive applications [
The model is executed as follows. Whenever the user performs a specific gesture matching an expected outgoing gesture from the currently active state, the active state changes to the destination of the outgoing edge of the performed gesture. Global variables can be defined onGISMO models (e.g. nbarrow and power in Fig. 2). They store relevant information about the object being modeled. Triggering a state change can be conditioned by a boolean precondition that may combine the observed dimension of the gesture and the global variables. For example, a state change from Drawn to ArrowReady is triggered if the distance d of the drag gesture exceeds 30cm and the global variable nbarrow is strictly positive. Exit actions of a matching gesture can be executed to perform operations on a global variable, such as reassigning its value by the value retrieved from the observed dimension. In the example of Fig. 2, the two drag gestures connected to state Bending add or subtract from global variable power the value of the gesture’s distance dimension. 3
Enabling verification of domain-specific model properties requires a certain amount of
preparatory work in order to make it applicable in practice. In particular, the ProMoBox
approach [
This section focuses on the changes and simplifications required to the GISMO metamodel in order to enable specification and verification of domain-specific properties. A first simplification ignores thetime and speed dimensions of input gestures. Thus, we restrict ourselves to properties based on the distance dimension only. Moreover, as unbounded variable domains are too costly to check, we provided a binary classification of a gesture’s distance value into either small or big. A wider range of distance classes could be used, at the expense of a longer verification time.
As another simplification we limit the types of global variables to boolean values only, i.e., integer values are not supported during property verification. We also represent each global variable by a unique integer identifier instead of a variable name since strings are not supported by Promela, the verification modelling language to which our DSML models are translated. This is not a huge concern since it can be fully automated and made transparent for the DSML engineer.
Finally, we simplified the preconditions and exit actions of GISMO models. In GISMO, preconditions are boolean expressions resulting from the logical composition (AND, OR, NOT) of comparisons between global variables, gesture dimensions and integer values (e.g., nbarrow>0 & d>30 between Drawn and ArrowReady states in Fig. 2). Exit actions, on the other hand, can express assignment operations of global variables (e.g., power += d in the gestures linked to the Bending state). For model verification we limit the precondition checks to verifying if a global variable is true or false; and exit actions are limited to changes of the boolean value of the global variable. Generally speaking, most of the simplifications on theGISMO DSL can be semi-automated and applied to any DSL, thus reducing the task of the domain engineer. 4
Applying ProMoBox to GISMO
The ProMoBox framework [
A fully automated method specialises and integrates these languages to any given DSML, thus minimising the effort of the language engineer. This is realised by manually annotating the DSML metamodel entities (classes, associations and attributes) with the necessary stereotypes required for every language construct. Stereotype rt (for runtime) annotates metamodel entities that serve as output (e.g., a state variable); stereotype ev (for event) annotates entities that serve as input only (e.g., a marking); stereotype tr (for trigger) annotates static entities that may also serves as input (e.g., a transition event). More stereotypes could be envisioned, but the generation of the sub-languages currently only supports those three. Stereotypes ev and tr cannot be used jointly on the same metamodel entity.
Fig. 3 illustrates how to apply ProMoBox to GISMO. Only the grey parts of Fig. 3 need to be modelled explicitly, the white parts are generated from the annotated and simplified GISMO’ metamodel, shown in Fig. 1. Classes colored in grey have been removed by the simplification process; stereotype annotations have been added.
A family of languages is generated from GISMO’ using a template-based approach. This approach makes ProMoBox applicable to different types of DSMLs. The main idea is that generic metamodel elements (shown as grey rectangles in Fig. 4) are interwoven with the DSL metamodel elements.
As an example, Fig. 4 shows the metamodel of the generated output language
GISMOO. The metamodel of generated design language GISMOD closely resembles
GISMOO, except that the grey classes in the figure are absent, OutputElement is
replaced by DesignElement, and the isActive attribute of Element and the value attribute
of Bool is also absent, because of the rt annotations in Fig. 1. The metamodel of
generated runtime language GISMOR looks like GISMOO, except that the grey classes
are absent, and OutputElement is replaced by RuntimeElement. Fig. 2 shows an example
runtime instance model of GISMOR, representing a snapshot of the bow model during
its execution. The currently active state is displayed in green. The generated metamodel
of input language GISMOI is depicted in Fig. 4, together with an example instance
model. This model represents a sequence of a MoveGesture followed by two
DragGestures (each gesture is surrounded by a green circle) provided by the user as input and
processed by the operational semantics rules to execute the runtime model GISMOR.
The generated metamodel of property language GISMOP allows to define temporal
properties over the system behaviour by means of four constructs: quantification (∀ or
∃), temporal patterns, structural patterns and domain-specific pattern elements. These
property-related constructs are added to the GISMO’ metamodel by weaving the generic
metamodel template of Fig. 5 into the DSML. The resulting language has a concrete
syntax that highly corresponds to the DSML, and the quantification and temporal
patterns (instead of LTL operators) are raised to a more intuitive level by using natural
language. The full metamodel of GISMOP is not shown here, but a similar example can
be found in [
Properties specified in GISMOP are translated to LTL, and a Promela model is generated that includes a translation of the initialised system, the environment, and the rule-based operational semantics of the system. This translation is generic, and thus independent of the DSML. The properties are checked by the SPIN model checker. If any counter-example is found, the verification results are translated back to the DSM level.
The limitations of the framework are related to the mapping to Promela as explained
in [
We implemented the ProMoBox framework in AToMPM [
We verified fifteen properties on the runtime instance model of Fig. 2. Five properties are described below: P1 It is always possible to return to a previously active state.
P2 A bow cannot be bent if there is no arrow on it. (see Fig. 6 at the top left; the global variable nbarrow is represented by integer id 1).
P3 All states of a model can be reached from any state.
P4 Whenever the bow is fired, the amount of available arrows should decrement (see
Fig. 6 at the top right; the global variable nbarrow is represented by integer id 1). P5 After firing an arrow, one should eventually be able to fire another one.
The above properties are transformed to LTL, and are inserted in Promela code consisting of the initial state of the system, the environment and the rule-based operational Generated metamodel of output language GISMOO Generated metamodel of input language GISMOI
Example of an instance model of GISMOI
Fig. 4. Generated metamodels GISMOO and GISMOI , and instance model of GISMOI . Proceedings of MPM 2014 semantics as shown in step 1 of Fig. 3. In step 2, SPIN verifies whether the system satisfies the formula, returning “True” if it does. If there is a counter-example, steps 3 to 5 are followed: the counter-example trace is played back by SPIN, and a readable trace is printed (step 3), this trace is converted automatically to the counter-example output model (step 4), and this counter-example can be played out state by state by showing a runtime model for each state (step 5). The properties P2 and P4 yield a counter-example, one of which is shown in Fig. 6 at the bottom. The trace represents a sequence of five states, leading to the undesirable state (the last one, where the state is Bending, but the nbarrow variable has value 0). Each state can be mapped to Fig. 2, and the current state is highlighted, as well as the current input gesture. Because of these counter-examples, we were able to find and fix an error in our bow model of Fig. 2, namely that picking up an arrow (represented by the MoveGesture to the left of sheated) is not required. In another instance, we were able to find and correct an error in one of the operational semantics’ rules.
In comparison to [
In the last decade, a plethora of language-specific approaches have been presented to
specify and verify properties for different kinds of design-oriented languages. A
subset of these approaches verify component-based systems [
Generic solutions shift the specification and verification tasks to the model level in a
more generalized manner. Some approaches propose OCL extensions for defining
temporal properties (TOCL) on models [
This article reported on a practical application of the ProMoBox approach [
In future work, we are interested in broadening the types of languages that are supported by ProMoBox, e.g. languages and properties that explicitly include time. Also, we will investigate alternative approaches to model checking, such as the generation and execution of test cases, so that the approach becomes more scalable.