Formal Verification of Systems Modelled in fUML
- When?
- Thursday 13 January 2011, 09:30 to 10:30
- Where?
- 39BB02
- Open to:
- Students, Staff
- Speaker:
- Mr Islam Abdel Halim
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 work 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 FDR2 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. An optimization technique has been applied to model the communication mechanism, such that large models can be compiled and analyzed using FDR2.
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.
The Event-B formal language has been used to model the same part of Tokeneer, and we use ProB to compare the performance of the two model checkers (FDR2 and ProB). Several interesting findings and questions came out of this comparison.