2009 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プロトコルのエラー検出機構をすり抜ける通信路上のビットエラーを解析する手法を明かにした.実験の結果,設計時には想定していなかった見逃し誤りが存在することが示された.
・項書き換え系を応用した命令型プログラム検証に関する研究:命令型プログラムを等価な制約付き項書換え系に変換し,得られた制約付き項書換え系の性質を検証することでプログラムの性質を検証するという手法において重要な役割を果たす書換え帰納法のための自動補題生成法を開発した.
その他に,項書き換え系の非干渉性に関する研究,項書き換え系の停止性に関する研究,充足可能性判定に関する研究を行なった.
|
