Want tool to obtain linear temporal logic spec from UML 2.0 sequence diagram

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 开发者_JAVA技巧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.

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 !!

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?