pdfreaders.org

Monadic Sequence Testing and Explicit Test-Refinements

by Achim D. Brucker and Burkhart Wolff

Cover for brucker.ea:monadic-sequence-testing:2016.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)

QR Code for brucker.ea:monadic-sequence-testing:2016.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) (Share article on LinkedIn. Share article on CiteULike. )

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.},
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},
pdf = {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},
}