Monadic Sequence Testing and Explicit Test-Refinements.
Lecture Notes in Computer Science(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 relation to traditional, IO-automata based notions.
更多查看译文
关键词
Monadic sequence testing framework,HOL-TestGen
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要