基于属性的代码切片用于 OSEK/VDX 操作系统的高效验证
软件工程
2013-01-03 v1
摘要
测试是工业界事实上的验证技术，但因其乐观的不完备性，不足以识别细微问题。另一方面，模型检测是一种支持完备性的强大技术，因此适用于安全关键系统的验证。然而，它通常比测试需要更多的知识和成本。本工作试图结合这两种技术的优势，以实现基于 OSEK/VDX 的汽车操作系统的集成高效验证。我们提出了基于属性的环境生成和模型提取技术，利用静态代码分析，可同时应用于模型检测和测试。该技术已实现自动化，并应用于基于 OSEK/VDX 的汽车操作系统 Trampoline。使用随机测试和模型检测对 Trampoline 内核代码中的断言进行验证的对比实验表明，我们的环境生成和抽象方法如何被用于高效的故障检测。
引用
@article{arxiv.1301.0042,
title = {Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems},
author = {Mingyu Park and Taejoon Byun and Yunja Choi},
journal= {arXiv preprint arXiv:1301.0042},
year = {2013}
}
备注
In Proceedings FTSCS 2012, arXiv:1212.6574