Item type |
Symposium(1) |
公開日 |
2014-10-15 |
タイトル |
|
|
タイトル |
組込みアセンブリプログラムのモデル構築によるモデル検査 |
タイトル |
|
|
言語 |
en |
|
タイトル |
Model Checking by Modeling for Embedded Assembly Programs |
言語 |
|
|
言語 |
jpn |
キーワード |
|
|
主題Scheme |
Other |
|
主題 |
モデル検査 |
資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
著者所属 |
|
|
|
金沢大学 |
著者所属 |
|
|
|
金沢大学 |
著者所属 |
|
|
|
金沢大学 |
著者所属(英) |
|
|
|
en |
|
|
Kanazawa University |
著者所属(英) |
|
|
|
en |
|
|
Kanazawa University |
著者所属(英) |
|
|
|
en |
|
|
Kanazawa University |
著者名 |
公下, 亮佑
山根, 智
櫻井, 孝平
|
著者名(英) |
Ryosuke, Konoshita
Satoshi, Yamane
Kohei, Sakurai
|
論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
組込みシステムは,広く利用されており,徐々に複雑化している.複雑化している組込みシステムを安全に運用するためには,システムの安全性を保証することが重要である.複雑なシステムに対する検証手法として,モデル検査が有効である.我々は,組込みシステムのアセンブリプログラムの全振る舞いから,モデルを自動的に生成するツールを開発した.ツールによって生成されたモデルを,モデル検査器に入力することで,システムの安全性を保証する.また,状態爆発に対応するため,Delayed NonDeterminism をベースとした,不定値と呼ぶ抽象化手法を導入する. |
論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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 Behavior Extractor to automatically model all behaviors of embedded assembly programs. Then, we ensure the safety by model checkers. In addition, we have introduced the undefined value to reduce the number of states. The undefined value is based on the Delayed NonDeterminism. |
書誌情報 |
組込みシステムシンポジウム2014論文集
巻 2014,
p. 13-21,
発行日 2014-10-15
|
出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |