Comparative Experiment of SPIN and SMT in Model Checking of Embedded Assembly Program
Comparative Experiment of SPIN and SMT in Model Checking of Embedded Assembly Program
复制标题
SPIN与SMT在嵌入式汇编程序模型检验中的对比实验
DOI：
10.1109/gcce50665.2020.9291772
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Kosuke Uemura
中科院分区：
文献类型：
--
作者：
Satoshi Yamane;Kosuke Uemura
嵌入式软件具有依赖于硬件的特性，对消费电子产品很重要。嵌入式软件的形式化验证是有用的技术。本研究的目的是比较实验研究自旋和基于可满足模理论的嵌入式装配程序的有界模型检验（SMT-Based BMC）。我们的方法生成的模型包括中断。使用中断处理程序执行减少（IHER）来减小模型的大小。与使用基于smt的BMC相比，我们可以在更短的时间内使用SPIN验证汇编程序，但是基于smt的BMC更方便，因为它可以使用背景理论及其通用定理证明。
Embedded software, which has properties dependent on hardware, is important for Consumer electronics. Formal verifications of embedded software are useful techniques. Our study aims at comparative experimental study of SPIN and our Satisfiability Modulo Theories -Based Bounded Model Checking (SMT-Based BMC) of Embedded Assembly Program. The models are generated by our method include interrupts. The size of the models is reduced using Interrupt Handler Execution Reduction (IHER). We can verify assembly program using SPIN in less time than using our SMT-Based BMC, but our SMT-Based BMC is convenient because it can use background theories and its general purpose theorem provers.
嵌入式系统的模型检查 C 源代码
DOI：
--
发表时间：
2009
期刊：
International Journal on Software Tools for Technology Transfer (STTT)
影响因子：
--
作者：
Bastian Schlich;S. Kowalewski
通讯作者：
S. Kowalewski
基于SMT的带中断的嵌入式汇编程序有界模型检查
DOI：
10.1109/dasc/picom/cbdcom/cyberscitech.2019.00120
发表时间：
2019
期刊：
2019 IEEE Intl Conf on Dependable, Autonomic and Secure Computing
影响因子：
--
作者：
Kousuke Uemura;Satoshi Yamane:
通讯作者：
Satoshi Yamane: