Want a tool to get a linear temporal logic specification from a UML 2.0 sequence diagram

I am working on software consistency checking. for this I need to write linear temporal logic for the UML 2.0 sequence diagram. if any body has any other tool for the same answer as soon as possible. I will be very grateful to you. I found that the charmy tool has a plugin for the same. Does anyone have the source code for the enchanting tool (CHecking ARchitectural Model consistencY). It is not available on their website.

Thanks in advance.

+4
source share
2 answers

The sequence diagram model is unsuitable for me.

I mean, you might have a sequence diagram, but the base model is really messy. A sequence diagram is the only UML diagram whose model is not actually reused. Sorry for this post, but I think the sequence diagram should remain graphic because the metamodel was not well developed in the UML specification and it is too late to change it!

+2
source

I'm not sure I understand the problem. According to the wikipedia article , the sequence diagram has no cycles, so the corresponding LTL formula will not contain any diamonds or boxes, etc., It will be just a sequence of atomic events, no?

Could you give an example sequence diagram and the corresponding LTL formula?

0
source

Source: https://habr.com/ru/post/1310108/


All Articles