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
Categories:
Documents: (full text as PDF file)
Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff.
Monadic Sequence Testing and Explicit Test-Refinements.
In TAP 2016: Tests And Proofs. Lecture Notes in Computer Science (9762), Springer-Verlag, 2016.
Keywords: monadic sequence testing framework; HOL-TestGen
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-41135-4_2) (
| 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.}, | |
| address | = | {Heidelberg}, | |
| author | = | {Achim D. Brucker and Burkhart Wolff}, | |
| booktitle | = | {{TAP} 2016: Tests And Proofs}, | |
| doi | = | {10.1007/978-3-319-41135-4_2}, | |
| editor | = | {Bernhard K. Aichernig and Carlo A. Furia}, | |
| isbn | = | {978-3-642-38915-3}, | |
| keywords | = | {monadic sequence testing framework; HOL-TestGen}, | |
| language | = | {USenglish}, | |
| location | = | {Vienna}, | |
| number | = | {9762}, | |
| = | {https://www.brucker.ch/bibliography/download/2016/brucker.ea-monadic-sequence-testing-2016.pdf}, | ||
| publisher | = | {Springer-Verlag}, | |
| series | = | {Lecture Notes in Computer Science}, | |
| title | = | {Monadic Sequence Testing and Explicit Test-Refinements}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-monadic-sequence-testing-2016}, | |
| year | = | {2016}, |