University of Surrey

Test tubes in the lab Research in the ATI Dance Research

An integrated framework for checking the behaviour of fUML models using CSP

Abdelhalim, I, Schneider, SA and Treharne, H (2013) An integrated framework for checking the behaviour of fUML models using CSP International Journal on Software Tools for Technology Transfer, 15 (4). 375 - 396. ISSN 1433-2779

[img]
Preview
PDF
STTT-2012.pdf
Available under License : See the attached licence file.

Download (1MB)
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf

Download (33kB)

Abstract

Transforming Unified Modelling Language (UML) models into a formal representation to check certain properties has been addressed many times in the literature. However, the lack of automatic formalization for executable UML models and provision of model checking results as modeller-friendly feedback has inhibited the practical use of such approaches in real life projects. In this paper, we address those issues by performing the automatic formalization of the Foundational subset for executable UML (fUML) models into communicating sequential processes without any interaction with the modeller, who should be isolated from the formal methods domain. The formal analysis provides the modeller with a UML sequence diagram that represents the model checking result in the case where an error has been found in the model. This work also considers the formalization of systems that depend on asynchronous communication between components in order to allow checking of the dynamic concurrent behaviour of systems.We have designed a comprehensive framework that is implemented as a plugin to MagicDraw (the CASE tool we use) that we call Compass. The framework depends on Epsilon as a model transformation tool that utilizes the Model Driven Engineering approach. It also implements an optimization approach to be able to model check concurrent systems using FDR2, and at the same time comply with the fUML inter-object communication mechanism. In order to validate our framework, we have checked a Tokeneer fUML model against deadlock using Compass. The model checking results are reported in this paper showing the advantages of our framework.

Item Type: Article
Additional Information: The original publication is available at http://www.springerlink.com/content/l88340q740286441/
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Symplectic Elements
Date Deposited: 12 Oct 2012 10:12
Last Modified: 01 Aug 2014 01:08
URI: http://epubs.surrey.ac.uk/id/eprint/721387

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800