A holistic approach to test-driven model checking

Abstract

Testing is the most common validation method in the software industry. It entails the execution of the software system in the real environment. Nevertheless, testing is a cost-intensive process. Because of its conceptual simplicity the combination of formal methods and test methods has been widely advocated. Model checking belongs to the promising candidates for this marriage. The present paper modifies and extends the existing approaches in that, after the test case generation, a model checking step supports the manual test process. Based on the holistic approach to specification-based construction of test suites, this paper proposes to generate test cases to cover both the specification model and its complement. This helps also to clearly differentiate the correct system outputs from the faulty ones as the test cases based on the specification are to succeed the test, and the ones based on the complement of the specification are to fail. Thus, the approach handles the oracle problem in an effective manner. © Springer-Verlag Berlin Heidelberg 2005.