Beta: a B based testing approach

Abstract

Software systems are a big part of our lives and, more than ever, they require a high level of reliability. There are many software Verification and Validation (V&V) techniques that are concerned with quality control, security, robustness, and reliability; the most widely known are Software Testing and Formal Methods. Formal methods and testing are techniques that can complement each other. While formal methods provide sound mechanisms to reason about the system at a more abstract level, testing techniques are still necessary for a more in-depth validation of the system and are often required by certification standards. Taking this into consideration, BETA provides a tool-supported, model-based testing approach for the B Method that is capable of generating unit tests from abstract B machines. In this thesis, we present improvements made in the BETA approach and tool, and new cases studies used to evaluate them. Among these improvements, we integrated logical coverage criteria into the approach, reviewed the input space criteria that was already supported, and enhanced the final steps of the test generation process. The approach now has support for automatic generation of oracle data and test case preambles, it has a feature for test data concretization, and a module that automatically generates executable test scripts. Another objective of this thesis was to perform more complex case studies using BETA and assess the quality of the test cases it produces. These case studies were the first to evaluate the test generation process as a whole, from test case design to implementation and execution. In our last experiments, we assessed the quality of the test cases generated by BETA, considering each coverage criteria it supports, using code coverage metrics such as statement and branch coverage. We also used mutation testing to evaluate the ability of the generated test cases to identify faults in the model’s implementation. The results obtained were promising, showing that BETA is capable of detecting faults introduced by a programmer or code generation tool and that it can achieve good coverage results for a system’s implementation based on a B model.