Branch Sequence Coverage Criterion for Testing-Based Formal Verification with Symbolic Execution

In specification-based testing, a desirable goal is to generate adequate test data to test every defined functional scenario in which all of its implementation paths are covered. However, experience suggests that this is a rather ambitious criterion that can hardly be met in practice due to the potentially great number of test data required. To address this challenge, we propose a new coverage criterion called Branch Sequence Coverage (BSC), aiming to strike a good balance between the assurance of program quality and the number of test data required by automatically finding all the necessary symbolic paths. In this paper, we discuss the features of BSC and compare it with partition testing (PT). We also illustrate how BSC can be well incorporated into a recently developed testing method known as Testing-Based Formal Verification with Symbolic Execution (TBFV-SE) for verification of the correctness of paths. We mainly focus on the exploration of the theoretical aspect of BSC and finally present a small case study to display the efficiency of BSC testing.