| 講演名 | 2015-03-06 組込みアセンブリプログラムからのモデル抽出による記号モデル検査(離散事象システム及び一般) 加藤 友紀, 公下 亮佑, 櫻井 孝平, 山根 智, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 組込みシステムは,広く利用されており,徐々に複雑化している.複雑化している組込みシステムを安全に運用するためには,システムの安全性を保証することが重要である.複雑なシステムに対する検証手法として,モデル検査が有効である.我々は,組込みシステムのアセンブリプログラムの全振る舞いから,モデルを自動的に生成するツールの出力結果をNuSMVの入力に変換する言語変換器を開発した.ツールによって生成されたモデルをモデル検査器に入力することにより,システムの安全性および活性の検証を行える.また,状態爆発に対応するため,出力されたモデルの中で使われていない変数の削除を行っている. |
| 抄録(英) | Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for complex systems. Model checking is effective to ensure the safety for complex systems. We have developed SMV converter to change the output of the Behavior Extractor into the input of the NuSMV. We have introduced the dead variable reduction to reduce the number of states. |
| キーワード(和) | モデル検査 / 組込みシステム / アセンブリプログラム / NuSMV |
| キーワード(英) | Model Checking / Embedded System / Assembly Program / NuSMV |
| 資料番号 | MSS2014-102 |
| 発行日 |
| 研究会情報 | |
| 研究会 | MSS |
|---|---|
| 開催期間 | 2015/2/26(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Mathematical Systems Science and its applications(MSS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 組込みアセンブリプログラムからのモデル抽出による記号モデル検査(離散事象システム及び一般) |
| サブタイトル（和） | |
| タイトル（英） | |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 組込みシステム / Embedded System |
| キーワード(3)（和/英） | アセンブリプログラム / Assembly Program |
| キーワード(4)（和/英） | NuSMV / NuSMV |
| 第 1 著者 氏名（和/英） | 加藤 友紀 / TOMONORI Kato |
| 第 1 著者 所属（和/英） | 金沢大学自然科学研究科 Kanazawa University |
| 第 2 著者 氏名（和/英） | 公下 亮佑 / RYOSUKE Konoshita |
| 第 2 著者 所属（和/英） | 金沢大学自然科学研究科 Kanazawa University |
| 第 3 著者 氏名（和/英） | 櫻井 孝平 / KOHEI Sakurai |
| 第 3 著者 所属（和/英） | 金沢大学自然科学研究科 Kanazawa University |
| 第 4 著者 氏名（和/英） | 山根 智 / SATOSHI Yamane |
| 第 4 著者 所属（和/英） | 金沢大学自然科学研究科 Kanazawa University |
| 発表年月日 | 2015-03-06 |
| 資料番号 | MSS2014-102 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | 493 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |