Extracting information for correction of flaws from embedded system specification of practical scale by formal method

2014 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

形式手法