Research on Design Verification Process Using Model Checking
Project/Area Number |
19500035
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Research Field |
Software
|
Research Institution | The University of Electro-Communications (2008) National Institute of Informatics (2007) |
Principal Investigator |
TAHARA Yasuyuki The University of Electro-Communications, 大学院・情報システム学研究科, 准教授 (30390602)
|
Co-Investigator(Kenkyū-buntansha) |
本位田 真一 国立情報学研究所, アーキテクチャ科学研究系, 教授 (70332153)
|
Project Period (FY) |
2007 – 2008
|
Project Status |
Completed (Fiscal Year 2008)
|
Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2008: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2007: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
Keywords | 計算機システム / 情報システム / ソフトウェア開発効率化・安定化 / ソフトウェア学 / ソフトウェア検証 |
Research Abstract |
近年、ソフトウェアは大規模化、複雑化が進んでいることから、高信頼でかつ安全なソフトウェア設計を実施するために、モデル検査技術が有望視されている。本研究では、開発者に分かりやすい設計と、モデル検査に必要な抽象的数学理論のギャップを縮めるために、既存技術であるTemplate Semantics をベースとした、形式モデルの意味論を参照・変更可能な設計モデル検証プロセスを考案し、そのプロセスに基づく開発支援ツールのプロトタイプを開発した。
|
Report
(3 results)
Research Products
(7 results)