University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formally Verifying Behaviour of fUML Models Using CSP.

Abdelhalim, Islam E. (2012) Formally Verifying Behaviour of fUML Models Using CSP. Doctoral thesis, University of Surrey (United Kingdom)..

[img]
Preview
Text
27558180.pdf
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (13MB) | Preview

Abstract

Transforming 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 work we address those issues by performing the automatic formalization of the fUML (Foundational subset for executable UML) models into CSP (Communicating Sequential Processes) without any interaction with the modeller, who should be isolated from the formal methods domain. We mainly consider the formalization of systems that depend on asynchronous communication between components in order to allow checking of the dynamic concurrent behaviour of systems. We introduce also a novel approach for optimizing the generated CSP model using a group of mathematically proved optimization rules. The approach includes also providing the modeller with optimization advice for the fUML model to maximize the reduction in the state space. We design an integrated framework that handles the formalization, feedback and optimization tasks. It is implemented as a plugin to MagicDraw (the CASE tool we use) that we call Compass which depends on Epsilon as a model transformation tool that utilizes the MDE (Model Driven Engineering) approach. Compass depends on FDR2 to perform the model checking for the CSP models. In order to validate the approach and its implementation (Compass), we check three non-trivial case studies modelled in fUML. The formalization and the optimization results show the success for achieving our work objective.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors : Abdelhalim, Islam E.
Date : 2012
Additional Information : Thesis (Ph.D.)--University of Surrey (United Kingdom), 2012.
Depositing User : EPrints Services
Date Deposited : 24 Apr 2020 15:26
Last Modified : 24 Apr 2020 15:26
URI: http://epubs.surrey.ac.uk/id/eprint/855006

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