2009 Fiscal Year Final Research Report
Automatic verification method for large scale embedded object-oriented design based on predicate abstraction
| Project/Area Number |
19500025
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
YAMANE Satoshi Kanazawa University, 電子情報学系, 教授 (70263506)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Keywords | 組込みシステム / 述語抽象化検証 / オブジェクト指向 |
|---|
| Research Abstract |
リアルタイムオブジェクト指向言語を開発して、オブジェクトが生成消滅するシステムに対して、構造と時間の抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。
|
