Enhancing the Capability of Testing-Based Formal Verification by Handling Operations in Software Packages

Testing a program based on its specification is necessary to ensure that the program meets its desired functionality. Formal methods, based on some mathematical theories, are often used to enhance the quality of systems but suffer from difficulties in application. The Testing-Based Formal Verification (TBFV) is proposed as an alternative to ensure the correctness of all traversed program paths, but is limited and impractical due to the lack of the capability of dealing with operations (e.g., methods defined in classes) provided in software packages. In this paper, we provide an axiomatic approach to dealing with this problem so as to enhance the capability of the TBFV. In particular, we focus on the Vector, ArrayList, and LinkedList classes in Java. We present both an example to demonstrate how our approach works properly and two small experiments conducted to evaluate the performance of our approach by comparing it with the specification-based testing (SBT). The result shows that our approach is more than 30% superior to the SBT in bug detection.