%0 Conference Proceedings
%T A Mechanised Proof of an Adaptive State Counting Algorithm
%+ University of Bremen
%+ University of Sheffield [Sheffield]
%A Sachtleben, Robert
%A Hierons, Robert, M.
%A Huang, Wen-Ling
%A Peleska, Jan
%Z Part 4: Testing and Verification Techniques
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 31th IFIP International Conference on Testing Software and Systems (ICTSS)
%C Paris, France
%Y Christophe Gaston
%Y Nikolai Kosmatov
%Y Pascale Le Gall
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-11812
%P 176-193
%8 2019-10-15
%D 2019
%R 10.1007/978-3-030-31280-0_11
%K Complete test methods
%K Finite state machines
%K Reduction
%K Proof assistants
%K Isabelle/HOL
%K Mechanised proofs
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02526349/document
%2 https://inria.hal.science/hal-02526349/file/482770_1_En_11_Chapter.pdf
%L hal-02526349
%U https://inria.hal.science/hal-02526349
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-ICTSS
%~ IFIP-LNCS-11812