### Abstract

This entry provides executable formalisations of complete test generation algorithms for finite state machines. It covers testing for the language-equivalence and reduction conformance relations, supporting the former via the W, Wp, HSI, H, SPY and SPYH-methods, and the latter via adaptive state counting. The test strategies are implemented using generic frameworks, allowing for reuse of shared components between related strategies. This work is described in the author's doctoral thesis.

### License

BSD License

### Topics

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

### Session FSM_Tests

- Util
- Util_Refined
- FSM_Impl
- FSM
- Product_FSM
- Minimisation
- Distinguishability
- IO_Sequence_Set
- Observability
- Prefix_Tree
- Prefix_Tree_Refined
- State_Cover
- OFSM_Tables_Refined
- Prime_Transformation
- Convergence
- Convergence_Graph
- Empty_Convergence_Graph
- H_Framework
- SPY_Framework
- Pair_Framework
- Intermediate_Implementations
- Test_Suite_Representations
- Simple_Convergence_Graph
- Intermediate_Frameworks
- H_Method_Implementations
- HSI_Method_Implementations
- Partial_S_Method_Implementations
- SPY_Method_Implementations
- SPYH_Method_Implementations
- Test_Suite_Representations_Refined
- W_Method_Implementations
- Wp_Method_Implementations
- Backwards_Reachability_Analysis
- State_Separator
- Adaptive_Test_Case
- State_Preamble
- Helper_Algorithms
- Maximal_Path_Trie
- R_Distinguishability
- Traversal_Set
- Test_Suite
- Test_Suite_IO
- Test_Suite_Calculation
- Test_Suite_Calculation_Refined
- FSM_Code_Datatype
- Test_Suite_Generator_Code_Export

### Depends on

- Light-weight Containers
- Generating linear orders for datatypes
- Native Word

### Auto-related entries

- Formalisation of an Adaptive State Counting Algorithm
- JinjaDCI: a Java semantics with dynamic class initialization

## Cite

×

FSM_Tests-AFP

    @article{FSM_Tests-AFP,
      author  = {Robert Sachtleben},
      title   = {Verified Complete Test Strategies for Finite State Machines},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/FSM_Tests.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Aug 11, 2022 : Isabelle2021-1