安全な物理情報システムのための反例解釈の理論と実装

• Project/Area Number: 25K21179
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60050:Software-related
• Research Institution: Kyushu University
• Principal Investigator: 張 振亜 九州大学, システム情報科学研究院, 助教 (10971228)
• Project Period (FY): 2025-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2027: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2026: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2025: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
• Keywords: Counterexample / Formal specification / Cyber-physical systems

Outline of Research at the Start

This project aims for quality assurance by counterexample explanation: 1) we exploit, beyond safe or not, the causation information hidden in counterexamples, by inferring from formal specifications; 2) we debug and repair system-level faults, based on the causation information in counterexamples.