%0 Conference Proceedings
%T An Executable Mechanised Formalisation of an Adaptive State Counting Algorithm
%+ Faculty of Computer Science and Mathematics [Bremen]
%A Sachtleben, Robert
%Z Part 4: Testing Methods and Automation
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 32th IFIP International Conference on Testing Software and Systems (ICTSS)
%C Naples, Italy
%Y Valentina Casola
%Y Alessandra De Benedictis
%Y Massimiliano Rak
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-12543
%P 236-254
%8 2020-12-09
%D 2020
%R 10.1007/978-3-030-64881-7_15
%K Complete test methods
%K Finite state machines
%K Isabelle/HOL
%K Mechanised proofs
%K Proof assistants
%K Reduction
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03239826/document
%2 https://inria.hal.science/hal-03239826/file/497758_1_En_15_Chapter.pdf
%L hal-03239826
%U https://inria.hal.science/hal-03239826
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-ICTSS
%~ IFIP-LNCS-12543