Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions
Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions
复制标题
DOI：
10.3390/electronics9071060
复制
发表时间：
2020-06
期刊：
影响因子：
2.9
通讯作者：
S. Yamane;Junpei Kobashi;Kosuke Uemura
中科院分区：
文献类型：
--
作者：
S. Yamane;Junpei Kobashi;Kosuke Uemura
嵌入式软件的属性取决于硬件（地址空间的直接操作，内存映射I/O，中断等）。因此，从较短的开发和高可靠性的角度来看，对与这些特性相对应的正式验证方法的需求正在增加。我们的研究旨在使用基于满足模式理论的基于嵌入式组装代码的安全性模型检查（基于SMT的BMC）进行正式验证。我们提出的方法通过固定尺寸的比特矢量理论详细生成装配代码的模型。我们方法生成的模型包括中断，并且使用中断处理程序降低（IHER）技术减少了模型的大小。在本文中，我们通过结合了基于SMT的有界模型检查并减少中断处理程序执行的验证方法的验证方法。此外，我们通过使用原型模型检查器进行实验来显示我们方法的评估。
Embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.). Therefore, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our study aims at enabling a formal verification with Satisfiability Modulo Theories-Based Bounded Model Checking (SMT-Based BMC) of safety for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts, and the size of the models is reduced using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method of safety properties of embedded assembly program by combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions. Moreover, we show the evaluation of our method by experiments using prototype model checker.