| Popis: |
This paper describes a way based on operational semantics of π-calculus and uses TGG tool to formalize sequence diagrams to establish formal verification through model transformations. Our transformation uses basic interactions and combined fragments with the operator Alt , Opt and Par . We argue that TGG rules can be more easily used and they become more understandable. The transformation feasibility is illustrated on a scenario of phone system. |
