仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用

2008 Fiscal Year Annual Research Report

• Project/Area Number: 20300006
• Research Institution: Chiba University
• Principal Investigator: 山本 光晴 Chiba University, 大学院・理学研究科, 准教授 (00291295)
• Co-Investigator(Kenkyū-buntansha): 萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252) ; 高橋 孝一 産業技術総合研究所, システム検証研究センター, 副研究センター長 (40357372) ; アルト シリル 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
• Keywords: モデル検査 / 仮想計算機

Research Abstract

本年度の成果は、1)各種仮想計算機の調査2)キャッシュ層の拡張3)ネットワークアプリケーションのモデル検査に対する各種アプローチの特徴付けとその考察に大別される。
本研究の目的は、a)仮想計算機技術を拡張・発展させることにより、プログラムの実行を遡る「バックトラッキング」を、通信を含むネットワークアプリケーションにおいても可能にすることb)上記のバックトラッキングをソフトウェアモデル検査に応用し、ネットワークアプリケーションの効率的な検証を可能にすることであった。この目的を達成するため、初年度である今年度は、まず各種仮想計算機実装の調査を行った。特に、バックトラッキングに必要なサスペンド・レジューム・マイグレーション機能について調査した。バックトラッキングを用いる第一義的な動機は、従来手法のキャッシュ層を用いたネットワークアプリケーションのモデル検査における、通信におけるメッセージ列が一定でなければならないという制約を回避するというものであったのだが、キャッシュ層自体を拡張することにより、この制限を緩和することに成功した。この成果により、仮想計算機を用いる初期の意義付けが曖昧になったため、その意義を今一度明確にする必要が生じた。このため、ネットワークアプリケーションのモデル検査に対する各種アプローチの特徴付けとその考察を行い、どのような種類のアプリケーションでどのようなアプローチが必要となるかを明確にした。2点目、3点目の成果については、今年度中の発表等はないが、論文を現在投稿中である。
連携研究者東京大学大学院情報理工学系研究科 田辺良則。
研究協力者東京大学大学院情報理工学系研究科 レオンワタナキット ワチャリン