通过符号执行自动生成安全关键软件的测试用例
软件工程
2022-09-23 v1
摘要
基于符号执行的自动化测试生成有利于对安全关键软件进行系统性测试，帮助测试工程师满足认证标准所要求的严格测试需求，同时控制测试过程的成本。与此同时，安全关键软件的开发常受编程语言或编码规范的约束，这些规范禁用被认为会降低程序安全性的语言特性，例如不允许动态内存分配和变长数组、限制循环使用方式、禁止递归并限制控制条件的复杂度。事实上，这些语言特性也正是当前基于符号执行的测试生成方法的主要效率阻碍。本文针对一类重要的工业安全关键系统，提供了利用符号执行生成测试用例有效性的新证据。我们特别关注 Scade——一种被广泛采用的面向安全关键嵌入式软件的基于模型的开发语言，并报告了一个案例研究，其中我们利用符号执行为一组用 Scade 开发的安全关键程序自动生成测试用例。为此，我们介绍在近期一个针对用 Scade 编写的安全关键铁路软件测试的工业项目中开发的新型测试生成器，并报告将该测试生成器用于测试属于高铁车载信号单元开发的一组 Scade 程序的经验。结果从经验上证明，符号执行确实是针对我们所考虑案例研究中安全关键程序生成高质量测试套件的可行方法。
引用
@article{arxiv.2209.11138,
title = {Automatically Generating Test Cases for Safety-Critical Software via Symbolic Execution},
author = {Elson Kurian and Daniela Briola and Pietro Braione and Giovanni Denaro},
journal= {arXiv preprint arXiv:2209.11138},
year = {2022}
}