プロセス代数CSPによるシーケンス図設計の詳細化と検証

摘要

ソフトウェアのモジュール構造の設計には，シーケンス図が用いられる場合が多い．本論文では，プロセス代数CSP を利用して．複数のシーケンス図から並行システムを合成し，詳細化関係の正しさや設計が要求を満たすかを検証する手法を提案する．本手法では，シーケンス図の合成に適した新しい演算子をCSP に追加する．また，この手法を実現するツールを開発し，効果を確認したことを報告する．%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, you can synthesize concurrent systems from multiple sequence diagrams. We define a new CSP operator for the synthesis of sequence diagrams. We also developed a tool to achieve this technique, and confirmed effectiveness of this approach.