Research on the verification of highly parallel and concurrent embedded software
| Project/Area Number |
20680001
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
AOKI Toshiaki 北陸先端科学技術大学院大学, 情報科学研究科研究科, 准教授 (20313702)
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥24,700,000 (Direct Cost: ¥19,000,000、Indirect Cost: ¥5,700,000)
Fiscal Year 2011: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2010: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
Fiscal Year 2009: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000)
Fiscal Year 2008: ¥8,060,000 (Direct Cost: ¥6,200,000、Indirect Cost: ¥1,860,000)
|
|---|
| Keywords | 形式手法 / 形式検証 / モデル検査 / ソフトウェア工学 / ソフトウェア開発効率化・安定化 / ディペンダブル・コンピューティング |
|---|
| Research Abstract |
We focus on parallel/concurrent software which is controlled by real-time operating system(RTOS) and RTOS itself. We have proposed an algorithm and tool to verify the behavior of parallel/concurrent software which contains scheduling by RTOS and real-time for the former. For the latter, we have proposed a method and tools to verify the design and implementation of RTOS. In addition, we have applied those method and tools to RTOS products. We succeeded in proposing verification methods based on model checking in practical settings and conducted that they are applicable to practical software products.
|
Report
(6 results)
Research Products
(60 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Book] 近代科学社2008
Author(s)
吉岡信和, 青木利晃, 田原康之
Total Pages
226
Publisher
SPINによる設計モデル検証
Related Report
-
