This module is being developed by Amir M. Saeidi under supervision of Prof. Sanjiva Prasad as part of Master's Thesis at Indian Institute of Technology, Delhi, India.
The goal of this project is to integrate model checking with ArgoUML. This is done by automatic translation of UML model to model checker's input notation. Once the model is translated and the properties to be checked are provided, the model checker is executed to verify the properties.
The model checker I am currently using is NuSMV. However, this can be extended for other model checking tools such as SPIN.
The translator for model checker uses the class diagram for the static structure of the system, and the statechart diagram for the dynamic behaviour of the system.
Before translation could be performed, UML model has to be validated. The validation consists of the following steps:
Once the UML model is validated, the translation process begins by transforming the static structure of the UML model, and then performing code generation.
For each class, a module is created, and the dynamic behaviour of the class specified by the statechart diagram is translated within the module.
I am completely open for new Ideas. So, if you would like to propose a new code generation strategy or you would like to share your works with me or anything that would contribute towards the project, please go ahead and contact me.
There are a few issues that I would like to share with you:
If you have any suggestions regarding the above issues, please come forward and let me know.
Anybody willing to help with developing the model checker module is highly welcomed. Please, send me a mail and we'll figure out how we could collaborate.