Hi Amir, it's been a long time ago when I had to deal with model checking.
> 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! I'd guess that a state diagram is best here, since the counter example strongly refers to the inner state of the model. Constructing a state machine for the counter example is not trivial, though. Even defining the states is not trivial. > 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. I have no clue, seems to depend on how the properties and all relevant attributes of the system are modelled? > 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? Ah, temporal logic! Inside ArgoUML, we only have OCL, so maybe a mapping needs to be found? Also times and time intervals need to be modelled somehow, otherwise a mapping would make no sense. (I hope my answers make sense, btw.) Did you check that UML (a notation for models of object oriented systems) is the right way to go for model checking? I have no overview here. Regards, Thomas -- GRATIS für alle GMX-Mitglieder: Die maxdome Movie-FLAT! Jetzt freischalten unter http://portal.gmx.net/de/go/maxdome01 ------------------------------------------------------ http://argouml.tigris.org/ds/viewMessage.do?dsForumId=450&dsMessageId=2566138 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]]
