Monadic Sequence Testing and Explicit Test-Refinements
Achim D. Brucker und 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.
Schlüsselwörter: monadic sequence testing framework; HOL-TestGen
Kategorien:
Dokumente: (Artikel als PDF Datei)
Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff.
Monadic Sequence Testing and Explicit Test-Refinements.
In TAP 2016: Tests And Proofs. Lecture Notes in Computer Science (9762), Springer-Verlag, 2016.
Schlüsselwörter: monadic sequence testing framework; HOL-TestGen
(Artikel als PDF Datei) (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}, |