### Abstract

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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Computer science/Algorithms

### Session Adaptive_State_Counting

- FSM
- FSM_Product
- ATC
- ASC_LB
- ASC_Suite
- ASC_Sufficiency
- ASC_Hoare
- ASC_Example

### Depends on

- Transition Systems and Automata

### Auto-related entries

- Verified Complete Test Strategies for Finite State Machines

## Cite

×

Adaptive_State_Counting-AFP

    @article{Adaptive_State_Counting-AFP,
      author  = {Robert Sachtleben},
      title   = {Formalisation of an Adaptive State Counting Algorithm},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Adaptive_State_Counting.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Aug 19, 2019 : Isabelle2019