Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP

Tomohiro KAIZU  Yoshinao ISOBE  Masato SUZUKI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E96-A   No.2   pp.495-504
Publication Date: 2013/02/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E96.A.495
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)
Category: Concurrent Systems
Keyword: 
sequence diagram,  process algebra,  CSP,  process synthesis,  

Full Text: PDF>>
Buy this Article




Summary: 
Sequence diagrams are often used in the modular design of softwares. In this paper, we propose a method to verify correctness of sequence diagrams. With this method, using the process algebra CSP, concurrent systems can be synthesized from a number of sequence diagrams. We define new CSP operators for the synthesis of sequence diagrams. We also report on a tool implementing our synthesis method and demonstrate how the tool analyzes sequence diagrams.