Automatic Invariant Testing for Finite-State Machines
summary
Tool automatically generates unit tests for state invariants by traversing a machine’s transition relation in an FSM DSL in Racket, removing dead states, and doing a BFS of paths up to a bounded number of rule reuses. Empirical run on 17 textbook machines shows running with default max rule application = 1 finishes under a second for most examples, while allowing two uses becomes often infeasible (out-of-memory). Implementation returns failing (state,word) pairs so students see concrete counterexamples.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:26Testing invariant predicates
- 2:50FSM implementation workflow
- 4:17Invariant predicate testing demo
- 5:43Tool implementation phases
- 8:15Tool practicality in classrooms
- 10:41Default settings and performance
- 12:46Live tool demo
- 14:54Comparison with existing tools
- 15:59Conclusion and future work
- 16:41Q&A
related talks
25mMastering UIs with Finite State Machines
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
20mAutomatic Repair of Regular Expressions
27mWrite Fewer Tests! From Automation to Autogeneration
26mThe missing piece of testing
41mImprove your Tests with Property State-Machine Tests
29mReactive State Machines and Statecharts
38mState of the Art Web User Interfaces with State Machines