An integrated framework for checking the behaviour

Authors: Islam Abdelhalim Steve Schneider Helen Treharne

Publish Date: 2012/06/28

Volume: 15, Issue: 4, Pages: 375-396

PDF Link

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 modellerfriendly 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 interobject 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

Keywords: