Extracting information for correction of flaws from embedded system specification of practical scale by formal method
| Project/Area Number |
24500032
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
HAGIHARA Shigeki 東京工業大学, 情報理工学(系)研究科, 助教 (70334547)
|
|---|
| Research Collaborator |
SHIMAKAWA Masaya 東京工業大学, 大学院情報理工学研究科, 研究員 (00749161)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Project Status |
Completed (Fiscal Year 2014)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2012: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 形式手法 / 組み込みシステム仕様 / 修正情報抽出 / 時間論理 / オートマトン / 極小充足不能集合 / 組込みシステム仕様 |
|---|
| Outline of Final Research Achievements |
For developing safety-critical embedded systems, verifying specification is expected to reduce the development costs of embedded systems. If a specification has flaws, we must correct the specification. It is desirable to obtain the cause and the location of flaws in the specifications. In this research, we proposed methods for obtaining the cause and the location and of flaws. In our methods, we manipulate omega-automata representing the specification to compute such information. We developed new reduction techniques for automata, and make such information computable for specifications of embedded systems at non-trivial scales. We proved correctness of our methods and clarified the time complexity of our methods. We also implemented our methods and got the tools.
|
Report
(4 results)
Research Products
(35 results)
