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
|
| Project Status |
Completed (Fiscal Year 2009)
|
| Budget Amount *help |
¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2007: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 組込みシステム / 述語抽象化検証 / オブジェクト指向 / リアルタイムオブジェクト指向 / 抽象化精錬検証 / 構造とリアルタイム性の抽象化 / 動的リアルタイムCEGAR / モデル検査 / オブジェクトの生成消滅 / 動的再構成組込みシステム / ハイブリッドオートマトン / 仕様記述言語 / 検証 / 述語抽象化洗練 |
|---|
| Research Abstract |
リアルタイムオブジェクト指向言語を開発して、オブジェクトが生成消滅するシステムに対して、構造と時間の抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。
|
Report
(4 results)
Research Products
(38 results)
-
-
-
[Journal Article]2010
Author(s)
山根智(分担)(共著)
-
Journal Title
電子情報通信学会ハンドブック/知識ベース (オーム社) (電子版公開予定)
Pages: 1-6
Related Report
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] 確率時間CEGAR2009
Author(s)
森下篤, 駒形龍太, 山根智
Organizer
電子情報通信学会研究報告
Place of Presentation
名古屋大学(愛知県)
Year and Date
2009-11-26
Related Report
-
[Presentation] 確率時間CEGAR2009
Author(s)
森下篤, 駒形龍太, 山根智
Organizer
電子情報通信学会
Place of Presentation
名古屋大学 (愛知県)
Year and Date
2009-11-26
Related Report
-
-
-
-
-
-
-
-
-
-
-
