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

https://hal.inria.fr/hal-02526349
Contributor : Hal Ifip <>
Submitted on : Tuesday, March 31, 2020 - 3:13:54 PM
Last modification on : Tuesday, March 31, 2020 - 3:59:18 PM

File

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

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Robert Sachtleben, Robert 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⟩

Share

Metrics

Record views

45