An integrated framework for checking the behaviour of fUML models using CSP
Abdelhalim, I, Schneider, SA and Treharne, H (2012) An integrated framework for checking the behaviour of fUML models using CSP International Journal on Software Tools for Technology Transfer, volume forthcoming . ISSN 1433-2779
Available under License : See the attached licence file.
Official URL: http://dx.doi.org/10.1007/s10009-012-0243-0
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.
|Additional Information:||The original publication is available at http://www.springerlink.com/content/l88340q740286441/|
|Divisions:||Faculty of Engineering and Physical Sciences > Computing Science|
|Deposited By:||Symplectic Elements|
|Deposited On:||12 Oct 2012 11:12|
|Last Modified:||16 Feb 2013 15:13|
Repository Staff Only: item control page