2008 Fiscal Year Annual Research Report
項書換え系と木オートマトンに基づくプログラム安全性検証に関する研究
| Project/Area Number |
20300010
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 Nagoya University, 大学院・情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Keywords | 安全性 / 項書き換え系 / 木オートマトン / モデル検査 / 車載LANプロトコル |
|---|
| Research Abstract |
本研究の目的は,項書換え系や木オートマトンの解析技法を応用し,通信プロトコルを始めとするネットワークソフトウエアを含む並行プログラム一般の安全性について,効率的かつ適用範囲の広い検証技法を確立するとともに,検証システムを実装,評価することである.
今年度行なった主な研究は以下のとおりである.
●ビットエラー環境下での新世代車載LANプロトコルの動作解析に関する研究:通信路でビットエラーが発生した場合のプロトコルの振る舞いをモデル検査ツールを用いて網羅的に解析する手法を明らかにした.この結果は,新世代車載LANプロトコルが安全に振る舞うこと検証するための基礎となる結果である.通信エラーの確率モデルを与えて,ビットエラーがプロトコルのアプリケーションに影響を与える可能性を解析することは今後の課題である.
●項書き換え系を応用した手続き型プログラム検証に関する研究:プログラムを等価な振る舞いをする制約付き項書換え系に変換し,得られた制約付き項書換え系の性質の証明技法を応用してプログラムの性質を検証する手法を開発し,実装作業を開始した.この結果をプログラムの安全性の検証に応用することは今後の課題である.
その他に,項書き換え系の停止性に関する研究,充足可能性判定に関する研究も行なった.
|
