Formal verification of MagicDraw statecharts

OData support
Supervisor:
Farkas Rebeka Krisztina
Department of Measurement and Information Systems

The development of complex systems makes it neccessary to gain access to modern modelling tools that support functionalities like validation, code generation and verification. One of the most well-known tool in the indsutry is MagicDraw: a tool for desinging systems and to model their behavior. MagicDraw is often used during the development of fault tolerant systems where it is mandatory to ensure that the system operates correctly.

Although MagicDraw is very rich in functionalities it lacks the ability to perform formal verification. The use of such methods would be highly beneficial for industrial use. Gamma is a modelling tool developed at the Department which is not as extensive in functions as MagicDraw is but it does support the verification of behavioral models. In my work I supporting formal verification of MagicDraw by creating a transformation between models of the two tools.

In this thesis I introduce Gamma and Magicdraw tools and the background knowledge needed to understand the transformation method. Furhtermore I describe in details the concepts and techologies used in my implementation. I describe the method via an example and I evaluate the results based on theoretical considerations. The presented product enables the formal verifications on a wider set of models.

Downloads

Please sign in to download the files of this thesis.