Verifying safety properties of embedded assembly program using innovative software model checking
| Project/Area Number |
15K00093
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2015: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
|---|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / ＳＭＴ / 定理証明 / 動的プログラム解析 / SMT / プログラム解析 |
|---|
| Outline of Final Research Achievements |
The research outcome can be roughly divided into the following two.
(1) We have developed a minimal model constructor (constructing a minimum model with interrupt processing embedded from the assembly program) by pruning and abstraction of dynamic program analysis and execution time estimation.
(2) SMT model checking method based on Abstraction and Refinement (CEGAR) was developed. This model checking method consists of predicate abstraction by SMT, SMT bounded model check, counter-example analyzer by SMT, and refinement predicate generation using Interpolation by SMT solver. As the SMT solver, Princess of Uppsala University which supports various interpolations was used.
|
Report
(4 results)
Research Products
(18 results)
