Theorem Prover-based Testing: Combining Verification and Testing

By Achim D. Brucker.

In this lecture, we will learn that testing and verification are not enemies. In fact, they are close friends that support us best in developing secure and correct systems when they work hand in hand. We will discuss the relationship of testing and verification both theoretically as well demonstrate HOL-TestGen, a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation.

The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs.

Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies – including security testing of network middleboxes.

Please cite this work as follows:
A. D. Brucker, “Theorem prover-based testing: Combining verification and testing,” presented at the Midlands graduate school, Leicester, UK, Apr. 09, 2017.

BibTeX
@Unpublished{ talk:brucker:tp-testing:2017,
  author     = {Achim D. Brucker},
  note       = {},
  date       = {2017-04-09},
  venue      = {Leicester, UK},
  eventtitle = {Midlands Graduate School},
  title      = {Theorem Prover-based Testing: Combining Verification and
                Testing},
  abstract   = {In this lecture, we will learn that testing and verification
                are not enemies. In fact, they are close friends that support
                us best in developing secure and correct systems when they
                work hand in hand. We will discuss the relationship of testing
                and verification both theoretically as well demonstrate
                HOL-TestGen, a specification and test case generation
                environment extending the interactive theorem prover
                Isabelle/HOL. As such, HOL-TestGen allows for an integrated
                workflow supporting interactive theorem proving, test case
                generation, and test data generation.
                
                The HOL-TestGen method is two-staged: first, the original
                formula is partitioned into test cases by transformation into
                a normal form called test theorem. Second, the test cases are
                analyzed for ground instances (the test data) satisfying the
                constraints of the test cases. Particular emphasis is put on
                the control of explicit test-hypotheses which can be proven
                over concrete programs.
                
                Due to the generality of the underlying framework, our system
                can be used for black-box unit, sequence, reactive sequence
                and white-box test scenarios. Although based on particularly
                clean theoretical foundations, the system can be applied for
                substantial case-studies -- including security testing of
                network middleboxes.},
  areas      = {software, security},
}