Verified Complete Test Strategies for Finite State Machines

Robert Sachtleben 📧

August 9, 2022


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


Theories of FSM_Tests