Specification-Driven Conformance Checking for Virtual/Silicon Devices Using Mutation Testing
Specification-Driven Conformance Checking for Virtual/Silicon Devices Using Mutation Testing
复制标题
使用变异测试对虚拟/硅设备进行规范驱动的一致性检查
DOI：
10.1109/tc.2020.2988906
复制
发表时间：
2021-03
影响因子：
3.7
通讯作者：
Fei Xie
中科院分区：
文献类型：
--
作者：
Haifeng Gu;Jianning Zhang;Mingsong Chen;Tongquan Wei;Li Lei;Fei Xie
现代软件系统，无论是系统软件还是应用软件，越来越多地在虚拟化软件平台上开发。它们可能只是打算在虚拟机上执行，也可能最终被期望移植到物理机上。在任何一种情况下，目标虚拟机或物理机中的虚拟或硅设备都应符合开发软件系统所基于的规范。这些设备不符合规范可能会导致软件系统的灾难性故障。在这篇文章中，我们提出了一个基于变异的框架，有效和高效的一致性检查之间的虚拟/硅设备的实现和他们的规格。基于我们定义的变异算子，设备规格可以自动仪表与弱的mutant-killing约束，以模拟潜在的错误设备行为。为了杀死所有可行的突变体，我们的方法采用了一个合作的符号执行机制，可以有效地自动化测试用例生成和一致性检查的虚拟/硅器件。通过象征性地执行仪表规格与虚拟/硅器件的轨迹从合作执行，我们的方法可以准确地衡量设计是否已经得到充分的验证，并报告设备规格和实现之间的不一致。在两个工业网络适配器及其虚拟设备上的综合实验证明了我们所提出的方法在虚拟设备和硅设备的一致性检查中的有效性。
Modern software systems, either system or application software, are increasingly being developed on top of virtualized software platforms. They may simply intend to execute on virtual machines or they may be expected to port to physical machines eventually. In either case, the devices, virtual or silicon, in the target virtual or physical machines are expected to conform to the specifications based on which the software systems have been developed. Non-conformance of these devices to the specifications can cause catastrophic failures of the software systems. In this article, we propose a mutation-based framework for effective and efficient conformance checking between virtual/silicon device implementations and their specifications. Based on our defined mutation operators, device specifications can be automatically instrumented with weak mutant-killing constraints to model potential erroneous device behaviors. To kill all feasible mutants, our approach adopts a cooperative symbolic execution mechanism that can efficiently automate the test case generation and conformance checking for virtual/silicon devices. By symbolically executing the instrumented specifications with virtual/silicon device traces obtained from the cooperative execution, our method can accurately measure whether the designs have been sufficiently validated and report the inconsistencies between device specifications and implementations. Comprehensive experiments on two industrial network adapters and their virtual devices demonstrate the effectiveness of our proposed approach in conformance checking for both virtual and silicon devices.
登录
查看更多内容
影响因子：
2
作者：
P. Mishra;Ronny Morad;A. Ziv;S. Ray
通讯作者：
P. Mishra;Ronny Morad;A. Ziv;S. Ray
DOI：
--
发表时间：
2012-10
期刊：
--
影响因子：
--
作者：
Matthew J. Renzelmann;Asim Kadav;M. Swift
通讯作者：
Matthew J. Renzelmann;Asim Kadav;M. Swift
DOI：
--
发表时间：
1996
期刊：
--
影响因子：
--
作者：
G. Rothermel;R. Untch
通讯作者：
G. Rothermel;R. Untch
DOI：
10.1007/978-3-319-89363-1_16
发表时间：
2018-04
期刊：
--
影响因子：
--
作者：
Bo Chen;Christopher Havlicek;Zhenkun Yang;Kai Cong;R. Kannavara;Fei Xie
通讯作者：
Bo Chen;Christopher Havlicek;Zhenkun Yang;Kai Cong;R. Kannavara;Fei Xie
DOI：
10.1145/154183.154265
发表时间：
1993-08
期刊：
--
影响因子：
--
作者：
R. Untch;Schemata A Jefferson Offutt;M. J. Harrold
通讯作者：
R. Untch;Schemata A Jefferson Offutt;M. J. Harrold