TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Aichernig, Bernhard K. ED - Furia, Carlo A. PY - 2016 DA - 2016// TI - Monadic Sequence Testing and Explicit Test-Refinements BT - TAP 2016: Tests And Proofs T3 - Lecture Notes in Computer Science IS - 9762 PB - Springer-Verlag CY - Heidelberg KW - monadic sequence testing framework KW - HOL-TestGen AB - 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. SN - 978-3-642-38915-3 L1 - https://www.brucker.ch/bibliography/download/2016/brucker.ea-monadic-sequence-testing-2016.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-monadic-sequence-testing-2016 UR - https://doi.org/10.1007/978-3-319-41135-4_2 DO - 10.1007/978-3-319-41135-4_2 LA - USenglish ID - brucker.ea:monadic-sequence-testing:2016 ER -