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?