History

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.

Mission

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.

Strategy

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:

• Syntactic Correctness: ensures that the specified UML model conforms to the abstract syntax of the UML metamodel (v1.4)
• Semantic Correctness: semantic check verifies a number of conditions that directly affects the translation
• Finite State Space: model checker requires the state space to be finite

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.

Contribution

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:

• Counterexample Representation in UML: There are two options to show the C/E given by model checker: one is to give the trace in textual format, the other is to represent it graphically using one of the diagrams, eg. Sequence Diagram. Sequence Diagram is not really a good option, because it does not show the internal behavior of the object at the time the inconsistency or error occurs.
• Incremental Checking: How do you think incremental checking can be performed, so that as soon as a property is falsified, a C/E is provided, bearing in mind that the model has to be weakly executable at the time translation is performed?
• Properties Specification: The properties must be expressed in terms of CTL or LTL. Not everyone knows how to write temporal logic. So, How should the users specify the properties?

If you have any suggestions regarding the above issues, please come forward and let me know.

How to Collaborate

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.

Related resources

• NuSMV Home Page