Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Formalisation of an Adaptive S...


view this post on Zulip Email Gateway (Aug 22 2022 at 20:25):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Formalisation of an Adaptive State Counting Algorithm
by Robert Sachtleben

This entry provides a formalisation of a refinement of an adaptive state
counting algorithm, used to test for reduction between finite state machines.
The algorithm has been originally presented by Hierons in the paper Testing from
a Non-Deterministic Finite State Machine Using Adaptive State Counting.
Definitions for finite state machines and adaptive test cases are given and many
useful theorems are derived from these. The algorithm is formalised using
mutually recursive functions, for which it is proven that the generated test
suite is sufficient to test for reduction against finite state machines of a
certain fault domain. Additionally, the algorithm is specified in a simple
WHILE-language and its correctness is shown using Hoare-logic.

https://www.isa-afp.org/entries/Adaptive_State_Counting.html

Enjoy,
René


Last updated: Mar 29 2024 at 12:28 UTC