記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証

• Item type: SIG Technical Reports(1)
• 公開日: 2008-09-19
• タイトル: 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証
• タイトル / 言語: en
• タイトル: Symbolic Model Checking of Consistency between Statemachine diagrams and Sequence diagrams
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 岡山県立大学大学院情報系工学研究科
• 著者所属: 岡山県立大学大学院情報系工学研究科
• 著者所属: 岡山県立大学大学院情報系工学研究科
• 著者所属: 岡山県立大学大学院情報系工学研究科
• 著者所属: 岡山県立大学大学院情報系工学研究科
• 著者所属(英): en
• 著者所属(英): Department of System Engineering, Faculty of Computer Science and System Engineering, Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Department of System Engineering, Faculty of Computer Science and System Engineering, Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Department of System Engineering, Faculty of Computer Science and System Engineering, Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Department of System Engineering, Faculty of Computer Science and System Engineering, Okayama Prefectural University
• 著者所属(英): en
• 著者所属(英): Department of System Engineering, Faculty of Computer Science and System Engineering, Okayama Prefectural University
• 著者名: 宮崎, 仁; 瀬古, 剛一; 横川, 智教; 佐藤洋一郎; 早瀬, 道芳
• 著者名(英): Hisashi, Miyazaki; Koichi, Seko; Tomoyuki, Yokogawa; Yoichiro, Sato; Michiyoshi, Hayase
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，UML の状態マシン図とシーケンス図で記述されたシステムを対象とし，システムの動作とモジュール間のモデルから求めるメッセージ通信順序の無矛盾性を検証する手法を提案している．提案手法では記号モデル検査ツール SMV を用いて検証を行う．そのため，まず，状態マシン図とシーケンス図からシステム全体の動作モデルを表す論理式を生成し，次に，シーケンス図からモジュール間のメッセージ通信の順序関係を表す論理式を生成する手法を提案している．さらに，検証する性質である設計間の無矛盾性の CTL 表現を与えている．最後に，例題システムに提案手法を適用し検証することで，本手法の有効性，妥当性を確認している．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a method to verify consistency between the transition relation and the sequence of software systems described by UML : statemachine diagrams and sequence diagrams. In order to use the symbolic model checker SMV, we first represent the transition relation of the system as a boolean formula, and then represent the sequence of messages exchanged between modules as a boolean formula. We also provided CTL formulas representing the consistency between the transition relation and the sequence. Finally, we show the availability of the proposed method by applying it to the watchdog mechanism.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 情報処理学会研究報告ソフトウェア工学（SE）; 巻 2008, 号 93(2008-SE-161), p. 41-47, 発行日 2008-09-19
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会