HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

An Executable Mechanised Formalisation of an Adaptive State Counting Algorithm

Abstract : This paper demonstrates the applicability of state-of-the-art proof assistant tools to establish completeness properties of a test strategy and the correctness of its associated test generation algorithms, as well as to generate trustworthy executable code for these algorithms. To this end, a variation of an established test strategy is considered, which generates adaptive test cases based on a reference model represented as a possibly nondeterministic finite state machine (FSM). These test cases are sufficient to check whether the reduction conformance relation holds between the reference model and an implementation whose behaviour can also be represented by an FSM. Both the mechanical verification of this test strategy and the generation of a provably correct implementation are performed using the well-known Isabelle/HOL proof assistant.
Complete list of metadata

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, May 27, 2021 - 4:43:07 PM
Last modification on : Thursday, May 27, 2021 - 4:58:36 PM
Long-term archiving on: : Saturday, August 28, 2021 - 8:00:23 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Robert Sachtleben. An Executable Mechanised Formalisation of an Adaptive State Counting Algorithm. 32th IFIP International Conference on Testing Software and Systems (ICTSS), Dec 2020, Naples, Italy. pp.236-254, ⟨10.1007/978-3-030-64881-7_15⟩. ⟨hal-03239826⟩



Record views