Information Technology Reference
In-Depth Information
to implement the automatic translation of xUML models to other target lan-
guages such as CSP [5] and mCRL2 [1] with our partners from the Universities
of Twente and Eindhoven. With respect to the validation of the translation,
we are currently using testing to guarantee that the translated model indeed
maintains the behaviour of the xUML model [16,18].
Another important future work is to revise our current translation to PRO-
MELA. For instance, one of the restrictions in our current work is the use of
global variables. This has direct consequences on the use of the Partial Order
Reduction algorithm found in SPIN. Therefore, if there are errors in the model
that can be easily detected, as in the Micro model shown in this paper, this
may not be a problem, since SPIN dynamically generates the state space dur-
ing verification stopping once an error is found. However, as the models have
fewer errors, checking the whole state space without the use of the Partial Order
Reduction algorithm may prove to be dicult, due to the increased state space.
Acknowledgment.
The work in this paper was funded by the European Com-
mission via the INESS project, Seventh Framework Programme (2008-2011).
References
1. Alexander, M., Gardner, W. (eds.): Process Algebra for Parallel and Distributed
Processing. CRC Press, USA (2008)
2. Artisan Software Tools Inc. Artisan studio UML modelling tool (2010),
http://www.artisansoftwaretools.com/
3. Formal Systems (Europe) Ltd. FDR 2.83 manual (2007)
4. Hardin, R.H., Har'El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A.
(eds.) CAV 1996. LNCS, vol. 1102, pp. 423-427. Springer, Heidelberg (1996)
5. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, USA (1985)
6. Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engi-
neering 23(5), 279-295 (1997)
7. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual.
Addison-Wesley, USA (2003)
8. INESS Project. INtegrated European Signalling System (INESS) Project Web Page
(2010),
http://www.iness.eu/
9. Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dy-
namic and hierarchical UML state machines. In: 3rd Workshop on Model design
and Validation, Italy, pp. 94-110 (2006),
http://modeva.itee.uq.edu.au/accepted_papers/main.pdf
10. KnowGravity Inc. Cassandra/xUML User's Guide (2008),
http://www.knowgravity.com/eng/value/cassandra.htm
11. Kolovos, D.S.: Extensible Platform for Specification of Integrated Languages for
mOdel maNagement Project Website (2010),
http://www.eclipse.org/gmt/epsilon
12. Kolovos, D.S., Paige, R.F., Polack, F.: Merging Models with the Epsilon Merg-
ing Language (EML). In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.)
MoDELS 2006. LNCS, vol. 4199, pp. 215-229. Springer, Heidelberg (2006)
