| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2015-03-06 13:55 組込みアセンブリプログラムからのモデル抽出による記号モデル検査 ○加藤友紀・公下亮佑・櫻井孝平・山根 智（金沢大）  MSS2014-102 |
|
| 抄録 | （和） | 組込みシステムは，広く利用されており，徐々に複雑化している．複雑化している組込みシステムを安全に運用するためには，システムの安全性を保証することが重要である．複雑なシステムに対する検証手法として，モデル検査が有効である．我々は，組込みシステムのアセンブリプログラムの全振る舞いから，モデルを自動的に生成するツールの出力結果を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 / / / / | |
| 文献情報 | 信学技報, vol. 114, no. 493, MSS2014-102, pp. 65-70, 2015年3月. | |
| 資料番号 | MSS2014-102 | |
| 発行日 | 2015-02-26 (MSS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | MSS2014-102 |
|
| 研究会情報 | |
| 研究会 | MSS |
| 開催期間 | 2015-03-05 - 2015-03-06 |
| 開催地（和） | ITビジネスプラザ武蔵 |
| 開催地（英） | IT Business Plaza Musashi |
| テーマ（和） | 離散事象システム及び一般、Work In Progress、計測と自動制御学会・離散事象システム部会と併催 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | MSS |
| 会議コード | 2015-03-MSS |
| 本文の言語 | 日本語 |
| タイトル（和） | 組込みアセンブリプログラムからのモデル抽出による記号モデル検査 |
| サブタイトル（和） | |
| タイトル（英） | The symbolic model checking by the model extraction from embedded assembly program |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 組込みシステム / Embedded System |
| キーワード(3)（和/英） | アセンブリプログラム / Assembly Program |
| キーワード(4)（和/英） | NuSMV / NuSMV |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 加藤 友紀 / Tomonori Kato / カトウ トモノリ |
| 第1著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 公下 亮佑 / Ryosuke Konoshita / コノシタ リョウスケ |
| 第2著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 櫻井 孝平 / Kohei Sakurai / サクライ コウヘイ |
| 第3著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 山根 智 / Satoshi Yamane / ヤマネ サトシ |
| 第4著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2015-03-06 13:55:00 |
| 発表時間 | 25分 |
| 申込先研究会 | MSS |
| 資料番号 | MSS2014-102 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | no.493 |
| ページ範囲 | pp.65-70 |
| ページ数 | 6 |
| 発行日 | 2015-02-26 (MSS) |
[研究会発表申込システムのトップページに戻る]