| Project/Area Number |
11480062
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
HAGIYA Masami Graduate School of Information Science and Technology, The University of Tokyo, Professor, 大学院・情報理工学系研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
YAMAMOTO Mitsuharu University of Chiba, Faculty of Science, Assistant, 理学部, 助手 (00291295)
TAKAHASHI Kouichi National Institute of Advanced Industrial Science and Technology, Chief researcher, 産業技術総合研究所, 主任研究員
TAMAI Tetsuo Graduate School of Interfaculty Initiative in Information Studies, The University of Tokyo, Professor, 大学院・情報学環, 教授 (60217172)
|
|---|
| Project Period (FY) |
1999 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥10,800,000 (Direct Cost: ¥10,800,000)
Fiscal Year 2001: ¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2000: ¥3,800,000 (Direct Cost: ¥3,800,000)
Fiscal Year 1999: ¥4,500,000 (Direct Cost: ¥4,500,000)
|
|---|
| Keywords | Verification / model checking / abstract interpretation / theorem proving / graph search / concurrent garbage / security / 並行ゴミ集め |
|---|
| Research Abstract |
This research investigated abstract model checking and related methods for verifying computational systems. Following are its major achievements.
We first proposed a general method for abstracting heap structures in order to verify algorithms that manipulate heap, such as concurrent garbage collection. In order to represent relationship between cells on heap, we devised a method to use regular expressions to characterize forward and backward connections from a cell.
As an application of abstract model checking, we proposed an analysis method called nonce analysis, which analyzes how nonces may leak, and combined it with the verification method based on strand spaces. In addition, in order to analyze probabilistic attacks or denial of service, we introduced the system of timed multiset rewriting and investigated its analysis methods.
As for discovering algorithms by model checking, we found several variants of on-the-fly and snapshot algorithms for concurrent garbage collection. We also tried to discover mutual exclusion algorithms, and actually found a variant of Dekker's algorithm under some special conditions. We also applied BDD (binary decision diagram) in order to speed up the search.
As for verification of model checking algorithms themselves, we introduced a framework with an abstraction relation among nodes in a graph, and formulated abstract model checking algorithms including covering graph construction. We applied the result to verification of timed automata. In particular, we formulated the algorithm for finding a state transition path with a minimal cost on a priced timed automation, i.e., timed automation with costs, as an instance of the abstract algorithm proposed by this research. We also formulated the A* version of the abstract algorithm and applied it to priced timed automata.
|
