Hello All The model checker tool that I'm currently working on, automatically translates UML model to model checker's input notation.
I've given a short description about the code generation strategy in the project web page, but there are a few remaining issues that I would like to share with you, hoping somebody may be able to help. 1. 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. Don't tell me I have to come up with a new diagram for UML! 2. 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. 3. 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? Cheers, Amir ------------------------------------------------------ http://argouml.tigris.org/ds/viewMessage.do?dsForumId=450&dsMessageId=2561962 To unsubscribe from this discussion, e-mail: [[email protected]]. To be allowed to post to the list contact the mailing list moderator, email: [[email protected]]
