Software model checking of real-time safety properties for embedded assembly program

2020 Fiscal Year Final Research Report

• Project/Area Number: 18K11239
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Kanazawa University
• Principal Investigator: Yamane Satoshi 金沢大学, 電子情報通信学系, 教授 (70263506)
• Co-Investigator(Kenkyū-buntansha): 櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
• Project Period (FY): 2018-04-01 – 2021-03-31
• Keywords: ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / SMT / Interpolation

Outline of Final Research Achievements

The purpose of this research is to formally verify real-time properties of embedded software that interacts with hardware and has severe timing constraints. The research objectives are to develop software model checking techniques for assembly programs, and to develop real-time safety verification for embedded assembly programs. (1) Transform assembly programs to generate the time Kripke structure, which is a formal semantic model of embedded software. (2) Based on theorem proving techniques, we develop a model checking technique for real-time embedded software by refining SMT predicate abstraction, SMT model checking, and SMT interpolation.

Free Research Field

ソフトウェア検証

Academic Significance and Societal Importance of the Research Achievements

現在のトヨタ車などのプログラム不具合の解消及び，今後の大規模ソフトウェアからなる
自動運転の安全性確保などの問題もあり，組込みソフトウェア安全性保証の研究は，社会的
かつ科学技術上の最重要な国際的課題である．従来の研究は仕様やＣプログラムの検証であり，組込みソフトウェアのハードウェアとの相互作用の検証やタイミング制約の検証が不十分である．本研究では，ハードウェアとの相互作用及びタイミング制約を検証するために，アセンブリプログラムを，形式的意味モデルである時間Kripke構造（アセンブリ命令の実行時間付き状態遷移システム）に変換して,リアルタイム性のソフトウェアモデル検査手法を開発することである