Skip to Main content Skip to Navigation
Conference papers

A Mechanised Proof of an Adaptive State Counting Algorithm

Abstract : In this paper it is demonstrated that the capabilities of state-of-the-art proof assistant tools are sufficient to present mechanised and, at the same time, human-readable proofs establishing completeness properties of test methods and the correctness of associated test generation algorithms. To this end, the well-known Isabelle/HOL proof assistant is used to mechanically verify a complete test theory elaborated by the second author for checking the reduction conformance relation between a possibly nondeterministic finite state machine (FSM) serving as reference model and an implementation whose behaviour can also be represented by an FSM. The formalisation also helps to clarify an ambiguity in the original test generation algorithm which was specified in natural language and could be misinterpreted in a way leading to insufficient fault coverage.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Tuesday, March 31, 2020 - 3:13:54 PM
Last modification on : Tuesday, March 31, 2020 - 3:59:18 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Robert Sachtleben, Robert M. Hierons, Wen-Ling Huang, Jan Peleska. A Mechanised Proof of an Adaptive State Counting Algorithm. 31th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2019, Paris, France. pp.176-193, ⟨10.1007/978-3-030-31280-0_11⟩. ⟨hal-02526349⟩



Record views


Files downloads