Information Technology Reference
In-Depth Information
timeout
keyword. This keyword is initially false, only becoming true when the
system gets to a stage where it can no longer progress (a deadlock occurs). The
timeout
keyword can then be used in a guard in order to ensure that the system
can progress.
2.3 Epsilon
Epsilon [11] is both a platform for task-specific model management languages
and a framework for implementing
new
model management languages by exploit-
ing the existing ones. Epsilon is currently a component of the Eclipse Genera-
tive Modeling Technologies (GMT) research incubator project. More specifically,
Epsilon provides a language for direct manipulation of models (EOL) [13], and
further languages for model merging (EML) [12], model comparison (ECL) [16],
model-to-model transformation (ETL) [17], model validation (EVL) [15] model-
to-text transformation (EGL) [22], model migration, and unit testing of model
management operations (EUnit).
EOL is the core language in Epsilon, providing OCL-like [20] model navigation
and modification facilities; all the other languages of the platform build on EOL
and its runtime environment in different ways. As a result, all the languages in
Epsilon are highly interoperable. For example, an
operation
defined using EOL
can be imported as-is by the model-to-model and the model-to-text transfor-
mation languages. Because all languages in Epsilon share a common runtime,
modules of different languages can exchange variables with each other [14]. With
regard to supported modelling technologies, the architecture of Epsilon allows
users to manage models of different technologies such as MDR and EMF models
and XML documents and even implement support for additional formats. In
this work we are using both model-to-model (ETL) and model-to-text (EGL)
transformation languages.
2.4 Related Work
Related work [28,9,27] has targeted the automatic verification of xUML models
using model-checking technology. The idea followed is basically the same, trans-
late xUML models to the input language of an existing model-checker that is
then used to analyse the model. In [28], the COSPAN model-checker [4] is used
as the target for the verification of xUML models. Similarly, the SPIN model-
checker [6] is used in [9]. Neither work uses transformation technology, nor does
either address certain features, like the use of derived attributes, of the xUML
action grammar that are used in the INESS models. More recent work trans-
latesxUMLmodelstoCSP
B [27,26], where the FDR model-checker [3] is then
used to analyse the system. This work uses model transformation, but the xUML
models being translated make substantially less use of the action language than
the railway signalling systems we are analysing.
||
