QuickCheck is well-known as a framework for Property-Based Testing whereby one writes tests as properties some code should respect and use generators and shrinkers to prove or find counterexamples to those properties. Building on those principles, quickcheck-dynamic is a new tool to define State-Machine like models of software, generate and run sequence of actions, and express properties of the system in terms of high-level Dynamic Logic expressions.
This session is both an introduction to, and an experience report on, the use of quickcheck-dynamic and more generally to the principles and practices of Model-Based Testing. Through a few examples drawn from real-life use of the library, I hope to convince the audience of the relevance of these tools for the development of complex, stateful software.