Specification-Driven Conformance Checking for Virtual/Silicon Devices Using Mutation Testing

摘要

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.