X. Cheng, N. He, and M.S. Hsiao (USA)
FCC, cognitive radio, mutation testing, model checking
In order to enhance the reliability of software defined radio and cognitive radio (CR), we designed, tested, and formally verified a software module called mask verifier to guarantee the legality of the output from the embedded software radio system with respect to the regulations. In order to validate the correctness of the mask verifier, we propose a hybrid two-stage testing and verification framework for validating the reliability of a CR system. Software Bounded Model Checking (BMC) as a formal verification technique is used in both stages. In the code validation stage, we combine unit testing with BMC for validating the mask verifier. In the other stage, we incorporate mutation testing with BMC for test suite refinement to improve the next iteration of code validation. Experiments show that such a hybrid framework is effective in uncovering hidden bugs and proving the correctness of the code with reduced computational costs.
Important Links:
Go Back
