| 講演名 | 2001/1/15 記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案 横川 智教, 土屋 達弘, 菊野 亨, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 高度な信頼性を要求されるハードウェア, ソフトウェアシステムの開発においては, システムが耐故障性を満たすことを形式的に証明することが必要とされている.本論文では, システムが耐故障性を満たしているか否かをモデル検査を用いて自動検証する手法の提案を行う.検証そのものには記号モデル検査をサポートするSMV(Symbolic Model Verifier)と呼ばれるツールを用いる.SMVはハードウェアシステムの検証のために開発され広く用いられており, ソフトウェアシステムの検証に用いられている例は少ない.ここでは, システムがガード付きコマンドによるプログラムでモデル化されていることを仮定して, そのモデルをSMVの入力言語によって表現する.そこで, まずそのモデルに基づいてシステムの記述を行うための言語を定義する.次に, その入力言語に従って記述されたシステムからSMV言語による記述へ変換するための手順を提案する.また, 文献から引用した例に対して提案法を適用した結果についても報告する. |
| 抄録(英) | We propose a model checking method for automatic verification of fault tolerance of systems. We assume that a system to be verified is given in the form of a guarded-command program. This method uses a symbolic model checking tool called SMV (Symbolic Model Verifier). Although it has been widely applied to hardware systems, it is rarely reported to apply to software systems. In this paper we define a modeling language suited for describing guarded command programs, and then we propose a translation method from the modeling language to the input language of SMV. Finally we apply the proposed method to an example in the literature to verify fault tolerance of the system. |
| キーワード(和) | 記号モデル検査 / 耐故障性 / SMV / 並行システム / BDD / 論理関数 |
| キーワード(英) | symbolic model checking / fault tolerance / SMV / concurrent system / BDD / boolean function |
| 資料番号 | SS2000-35 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2001/1/15(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 記号モデル検査を用いたシステムの耐故障性の自動検証手法の提案 |
| サブタイトル（和） | |
| タイトル（英） | Automatic Verification of Fault Tolerance Using Symbolic Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 記号モデル検査 / symbolic model checking |
| キーワード(2)（和/英） | 耐故障性 / fault tolerance |
| キーワード(3)（和/英） | SMV / SMV |
| キーワード(4)（和/英） | 並行システム / concurrent system |
| キーワード(5)（和/英） | BDD / BDD |
| キーワード(6)（和/英） | 論理関数 / boolean function |
| 第 1 著者 氏名（和/英） | 横川 智教 / Tomoyuki Yokogawa |
| 第 1 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 2 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 菊野 亨 / Tohru Kikuno |
| 第 3 著者 所属（和/英） | 大阪大学 大学院基礎工学研究科 情報数理系専攻 Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 2001/1/15 |
| 資料番号 | SS2000-35 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 569 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |