Dissertation
Specification-Based Testing with Büchi Automaton: Metrics, Tools and Performance Evaluation
Doctor of Philosophy (PhD), Washington State University
01/2015
Handle:
https://hdl.handle.net/2376/107834
Abstract
Testing and verification are two most frequently used verification and validation (V&V) techniques in software engineering. Traditional testing techniques have been well developed for decades, it is sometimes harder to pinpoint the defects of a software system, especially with regards to the requirements of the system. Specification-based testing has been widely studied in the academic field, to detect whether a system conforms to its specification. The idea is to tailor the testing process specifically towards the requirement specifications of the software system, hence rendering the testing process more valuable. While testing is useful in finding errors, it is less effective in showing the absence of bugs. Formal verification, on the other hand, uses mathematical proofs to establish the correctness of a software system with respect to certain properties. This dissertation proposes a novel approach to harness the synergy between testing and formal verification. In particular, we focus on integrating model checking with specification-based testing. Model checking is one of the most common used techniques of formal verification, and much research has been conducted on integrating model checking with testing. Our main contribution is a framework of test generation with respect to requirement specifications. Specifically, we base our work on specifications written as Büchi automata, a
powerful formal representation that is widely used in linear temporal logic model checking. With this framework, we dissect the structural elements of a
Büchi automaton for the purpose of test generation. Through this process, testing not only helps to identify errors in a system, it can also measure the degree of conformity of a system to its formal requirements, which in turn contributes to refining both the system and the requirements. We further demonstrate the effectiveness and efficiency of our approach through an extensive computational study.
Metrics
14 File views/ downloads
15 Record Views
Details
- Title
- Specification-Based Testing with Büchi Automaton: Metrics, Tools and Performance Evaluation
- Creators
- Bolong Zeng
- Contributors
- Li Tan (Advisor)Zhe Dang (Committee Member)David Bakken (Committee Member)Axel Krings (Committee Member)
- Awarding Institution
- Washington State University
- Academic Unit
- Electrical Engineering and Computer Science, School of
- Theses and Dissertations
- Doctor of Philosophy (PhD), Washington State University
- Number of pages
- 128
- Identifiers
- 99900581530501842
- Language
- English
- Resource Type
- Dissertation