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 relation to traditional, IO-automata based notions.
Author supplied keywords
Cite
CITATION STYLE
Brucker, A. D., & Wolff, B. (2016). Monadic sequence testing and explicit test-refinements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9762, pp. 17–36). Springer Verlag. https://doi.org/10.1007/978-3-319-41135-4_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
