University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP

Abdel Halim, I, Sharp, J, Schneider, S and Treharne, H (2010) Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP In: 12th International Conference on Formal Engineering Methods, 2010-11-17 - 2010-11-19, Shanghai, China.

icfem2010.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (338kB)
[img] Text (licence)

Download (1kB)


Much research work has been done on formalizing UML diagrams, but less has focused on using this formalization to analyze the dynamic behaviours between formalized components. In this paper we propose using a subset of fUML (Foundational Subset for Executable UML) as a semi-formal language, and formalizing it to the process algebraic specification language CSP, to make use of FDR as a model checker. Our formalization includes modelling the asynchronous communication framework used within fUML. This allows different interpretations of the communications model to be evaluated. To illustrate the approach, we use the modelling of the Tokeneer ID Station specifications into fUML, and formalize them in CSP to check if the model is deadlock free.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Abdel Halim, I
Sharp, J
Schneider, S
Treharne, H
Date : 2010
DOI : 10.1007/978-3-642-16901-4_25
Contributors :
Depositing User : Symplectic Elements
Date Deposited : 30 Sep 2011 14:21
Last Modified : 31 Oct 2017 14:09

Actions (login required)

View Item View Item


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