Monadic Sequence Testing and Explicit Test-Refinements

By Achim D. Brucker and Burkhart Wolff.

We present an abstract framework for sequence testing that is implemented in Isabelle/HOL-TestGen. Our framework is based on the theory of state-exception monads, explicitly modelled in HOL, and can cope with typed input and output, interleaving executions including abort, and synchronisation.

The framework is particularly geared towards symbolic execution and has proven effective in several large case-studies involving system models based on large (or infinite) state.

On this basis, we rephrase the concept of test-refinements for inclusion, deadlock and IOCO-like tests, together with a formal theory of its rela- tion to traditional, IO-automata based notions.

Keywords:
Monadic Sequence Testing Framework, HOL-TestGen

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Monadic sequence testing and explicit test-refinements,” in TAP 2016: Tests and proofs, B. K. Aichernig and C. A. Furia, Eds. Heidelberg: Springer-Verlag, 2016. doi: 10.1007/978-3-319-41135-4_2. Author copy: http://logicalhacking.com/publications/brucker.ea-monadic-sequence-testing-2016/

BibTeX
@InCollection{ brucker.ea:monadic-sequence-testing:2016,
  abstract  = {We present an abstract framework for sequence testing that is
               implemented in Isabelle/HOL-TestGen. Our framework is based on
               the theory of state-exception monads, explicitly modelled in
               HOL, and can cope with typed input and output, interleaving
               executions including abort, and synchronisation.
               
               The framework is particularly geared towards symbolic
               execution and has proven effective in several large
               case-studies involving system models based on large (or
               infinite) state.
               
               On this basis, we rephrase the concept of test-refinements for
               inclusion, deadlock and IOCO-like tests, together with a
               formal theory of its rela- tion to traditional, IO-automata
               based notions.},
  keywords  = {Monadic Sequence Testing Framework, HOL-TestGen},
  location  = {Vienna},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {{TAP} 2016: Tests And Proofs},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {9762},
  editor    = {Bernhard K. Aichernig and Carlo A. Furia},
  title     = {Monadic Sequence Testing and Explicit Test-Refinements},
  areas     = {formal methods},
  year      = {2016},
  doi       = {10.1007/978-3-319-41135-4_2},
  isbn      = {978-3-642-38915-3},
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-monadic-sequence-testing-2016/}},
}