2011 Fiscal Year Final Research Report
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
|
| 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.
|
