| 講演名 | 1999/1/22 記号モデル検査を用いたステートチャートの検証 寺田 博文, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 複雑なリアクティブシステムの仕様を簡潔に記述する手法として, ステートチャートを用いる方法が知られている.本論文では, ステートチャートで記述された仕様が与えられた場合に, その仕様が望ましい性質を満たしているかどうかを記号モデル検査(symbolic model checking)を利用して検証する方法について議論する.先ず, ヒストリー機能や, 状態遷移, 外部イベントといったステートチャートの主要な機能について, 検証ツールSMV(Symbolic Model Verifier)の入力言語(SMV言語)によって表現する方法を提案する.次に, 文献から引用した様々なリアクティブシステムのステートチャートによる仕様に対して, 提案法を適用してSMV言語に変換を行い, 更にデッドロックに陥らない等の性質についてSMVを利用して自動検証を行った.その結果, 比較的大きな仕様についても検証に必要な時間は30秒程度であり, 提案法が有効であることが確認できた. |
| 抄録(英) | Statechart is a well-known visual formalism for the specification and design of large and complex reactive systems. We discuss automatic verification of statechart specifications. Specifically, we use a symbolic model checking tool called SMV(Symbolic Model Verifier).Symbolic model checking overcomes the state explosion problem using the Binary Decision Diagram(BDD)to represent the transition relation and state space of the model.Although it has been highly successful when applied to hardware systems, it is rarely reported applying to software specifications. In this paper, we first propose a translation method from a statechart specification to the SMV language. Then, we apply the proposed method to examples of statecharts in the literature. |
| キーワード(和) | ステートチャート / 検証 / 記号モデル検査 / SMV / SMV言語 |
| キーワード(英) | statechart / verification / symbolic model checking / SMV / SMV language |
| 資料番号 | SS98-41 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1999/1/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 記号モデル検査を用いたステートチャートの検証 |
| サブタイトル（和） | |
| タイトル（英） | Verification of Statechart Specifications Using Symbolic Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | ステートチャート / statechart |
| キーワード(2)（和/英） | 検証 / verification |
| キーワード(3)（和/英） | 記号モデル検査 / symbolic model checking |
| キーワード(4)（和/英） | SMV / SMV |
| キーワード(5)（和/英） | SMV言語 / SMV language |
| 第 1 著者 氏名（和/英） | 寺田 博文 / Hirofumi Terada |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎光化学研究科情報数理系専攻 Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 2 著者 所属（和/英） | 大阪大学大学院基礎光化学研究科情報数理系専攻 Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru Kikuno |
| 第 3 著者 所属（和/英） | 大阪大学大学院基礎光化学研究科情報数理系専攻 Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 1999/1/22 |
| 資料番号 | SS98-41 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 558 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |