SDVerifier

Menu

• SDVerifier Editor
  • Edit sequence diagrams, convert them to PAT CSP, and analyze counter examples.
• SDVerifier Refinement Verifier
  • Merge two PAT CSP models for refinement checking. It generates (AbstractModel \ X) and (ConcreteModel \ X) where X is the set of events which the two models do not share.

Demo

• Sample 1
  • An example of eCommerce site. You can see counter example analyser here.
• Sample 2
  • An example of hotel reservation system.

References

• Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP
  • Tomohiro KAIZU, Yoshinao ISOBE, Masato SUZUKI (2013). IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences Vol.E96-A No.2 pp.495-504.
  • Paper (pdf) / IEICE Transactions Online
• Verifying sequence diagrams using the process algebra CSP
  • Tomohiro KAIZU, Yoshinao ISOBE, Masato SUZUKI (2013). AVOCS 2013 Automated Verification of Critical Systems Pre-proceedings pp.203-206.
  • Short paper (pdf)
• Definitions of the synthesis operators