SMT-Based Bounded Model Checking of Embedded Assembly Program with Interruptions
SMT-Based Bounded Model Checking of Embedded Assembly Program with Interruptions
复制标题
基于SMT的带中断的嵌入式汇编程序有界模型检查
DOI：
10.1109/dasc/picom/cbdcom/cyberscitech.2019.00120
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Satoshi Yamane:
中科院分区：
文献类型：
--
作者：
Kousuke Uemura;Satoshi Yamane:
嵌入式软件具有依赖于硬件的属性。我们的研究旨在使一个正式的验证与SMT为基础的有界模型检查的嵌入式汇编代码与嵌入式处理程序。我们提出的方法生成的汇编代码模型的详细与固定大小的位向量理论。我们的方法生成的模型包括中断，并减少使用中断执行减少（IHER）技术的模型的大小。本文提出了一种基于SMT的有界模型检测与可执行代码约简相结合的嵌入式汇编程序验证方法。此外，我们通过使用原型模型检查器的实验，我们的方法的评价。
Embedded software has properties dependent on hardware. Our study aims at enabling a formal verification with SMT-Based Bounded Model Checking of embedded assembly codes with Interrupt Handlers. 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 reduce the size of the models using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method 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.