| Project/Area Number |
20300006
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
YAMAMOTO Mitsuharu Chiba University, 大学院・理学研究科, 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HAGIYA Masami 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
ARTHO Cyrille 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
TANABE Yoshinori 国立情報学研究所, アーキテクチャ科学研究系, 特任准教授 (60443199)
TAKAHASHI Koichi 独立行政法人産業技術総合研究所, 情報技術研究部門, 情報戦略グループ長 (40357372)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Project Status |
Completed (Fiscal Year 2010)
|
| Budget Amount *help |
¥11,310,000 (Direct Cost: ¥8,700,000、Indirect Cost: ¥2,610,000)
Fiscal Year 2010: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2009: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2008: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
|
|---|
| Keywords | モデル検査 / 仮想計算機 / チェックポインティング |
|---|
| Research Abstract |
Model checking verifies program correctness using systematic/exhaustive search on the state space. In order to apply this technique to network applications, we implemented "communication backtracking" that rewinds the program execution including its communication states, and also included it as a module for Java PathFinder, a model checker for Java programs. Communication backtracking is implemented by running a communication peer program under a checkpointing environment, which enables us to save/restore program states, and providing an original transport layer in order to save/restore connections.
|
