一句话：提出 OiL-CEGAR，将形式化 OS 模型与抽象应用程序组合并按反例精化，提升多任务嵌入式软件模型检测的精度与效率。
多任务嵌入式软件的验证若忽略底层操作系统的调度策略与任务优先级处理，就难以获得足够精度；但把应用与完整 OS 一起验证又代价高昂、不切实际。本文提出 OiL-CEGAR（OS-in-the-Loop Counterexample-Guided Abstraction Refinement）：它将形式化 OS 模型与抽象后的应用程序组合起来进行整体验证，并利用该组合模型产生的反例逐步精化抽象；精化过程利用反例中的调度信息，将其视为一个 mini-OS，以检查反例轨迹在具体程序上是否可执行。原型实验表明，OiL-CEGAR 显著提升了该领域性质检查的准确性与效率：能自动消除所有误报，在一组多任务程序上平均 476 秒完成性质检查；而现有方法在同一组程序上准确率低于 11.1%，或因超时无法完成验证。
Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive verification of multitasking embedded software together with its underlying operating system is very costly and impractical. To reduce the verification cost while achieving the desired accuracy, we propose a variant of CEGAR, named OiL-CEGAR (OS-in-the-Loop Counterexample-Guided Abstraction Refinement), where a composition of a formal OS model and an abstracted application program is used for comprehensive verification and is successively refined using the counterexamples generated from the composition model. The refinement process utilizes the scheduling information in the counterexample, which acts as a mini-OS to check the executability of the counterexample trace on the concrete program. Our experiments using a prototype implementation of OiL-CEGAR show that OiL-CEGAR greatly improves the accuracy and efficiency of property checking in this domain. It automatically removed all false alarms and accomplished property checking within an average of 476 seconds over a set of multitasking programs, whereas model checking using existing approaches over the same set of programs either showed an accuracy of under 11.1% or was unable to finish the verification due to timeout.
DOI 原文 ·
@inproceedings{paperbot5201,
title = {Model Checking Embedded Control Software using OS-in-the-Loop CEGAR},
author = {Dongwoo Kim and Yunja Choi},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00059}
}