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

Content Provider	Springer Nature Link
Author	Abdelhalim, Islam Schneider, Steve Treharne, Helen
Copyright Year	2012
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.
Starting Page	375
Ending Page	396
Page Count	22
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	15
Issue Number	4
e-ISSN	14332787
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2012-06-28
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Formalization fUML CSP Deadlock Model checking FDR2 Tokeneer Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation
Content Type	Text
Resource Type	Article
Subject	Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Checking JML specifications using an extensible software model checking framework

Model checking of state-rich formalism by linking to $$CSP\,\Vert \,B$$

FDR3: a parallel refinement checker for CSP

Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more

Techniques for modelling and verifying railway interlockings

Schedulability of Herschel revisited using statistical model checking

An abort-aware model of transactional programming

Regular model checking

Incremental test case generation using bounded model checking: an application to automatic rating

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

Similar Documents

Checking JML specifications using an extensible software model checking framework

Model checking of state-rich formalism by linking to $$CSP\,\Vert \,B$$

FDR3: a parallel refinement checker for CSP

Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more

Techniques for modelling and verifying railway interlockings

Schedulability of Herschel revisited using statistical model checking

An abort-aware model of transactional programming

Regular model checking

Incremental test case generation using bounded model checking: an application to automatic rating

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