views:

71

answers:

2

i am working on checking model consistency of software. to do this i need to write linear temporal logic for UML 2.0 sequence diagram. if any body have any other tool for the same please response as soon as possible. I will be very obliged to you. i have found charmy tool have plugin for the same. Does anybody have source code for charmy tool(CHecking ARchitectural Model consistencY). It is not available on their website.

Thanks in advance.

A: 

I'm not sure I understand the problem. According to the wikipedia article, a sequence diagram does not have any loops, so the corresponding LTL formula would not contain any diamonds or boxes etc, it would just be a sequence of atomic events, no?

Could you please provide an example sequence diagram and corresponding LTL formula?

aioobe
You've misread. http://www.ibm.com/developerworks/rational/library/3101.html indicates that alternation and looping are possible.
Donal Fellows
Also, even with simple code there would still be a need for a good sprinkling of `◇` symbols; you can not count on the events from a sequence diagram happening immediately, so "eventually" is a useful modal operator. (God, I'm starting to remember some of this stuff…)
Donal Fellows
A: 

The sequence diagram model is for me unusable.

I mean that you can have a sequence diagram but the underlying model is really messy. The sequence diagram is the only UML diagram which model is not really reusable. Sorry for this post but I think that sequence diagram should remain graphical because the metamodel has not been well developped in the UML specification and it is too late to change it !!

Maybe it is not too late: http://www.drdobbs.com/architecture-and-design/224701702;jsessionid=OWQYMR1NPFHN1QE1GHRSKHWATMY32JVN
Gabriel Ščerbák