Verified Complete Test Strategies for Finite State Machines

Robert Sachtleben 📧

August 9, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session FSM_Tests