CSPを用いた状態マシン図とシーケンス図の整合性検証

• 横川, 智教

• 片山, 巧

• 宮崎, 仁

• 佐藤, 洋一郎

• 有本, 和民

書誌事項

タイトル別名

• Consistency veri cation of state machine diagrams and a sequence diagram using CSP

抄録

本稿では，UML の状態マシン図およびシーケンス図をプロセス代数形式のモデル記述言語であるCSP を用いて表現し，検証ツールFDR を用いて整合性検証を行う手法について示す．また，例題への適用実験を通して，整合性違反が存在する場合はそれを正しく検出できることを示している．

We propose a method to detect consistency errors in UML state machine diagrams and sequence diagrams by representing the diagrams as CSP, which is a process algebra style notation. We use FDR model checker to verify the consistency relation between the diagrams. We show an application example of the method where the correctness of consistencyof example diagrams is checked.

収録刊行物

• ウィンターワークショップ2014・イン・大洗 論文集

  ウィンターワークショップ2014・イン・大洗 論文集 2014 41-42, 2014-01-16

キーワード

• 形式手法

詳細情報

• CRID: 1050574047114101760
• NII論文ID: 170000080457
• Web Site: http://id.nii.ac.jp/1001/00097877/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles