PyModel: Model-based testing in Python

With model program and test harness in hand, developers or testers can use the tools of the model-based testing framework in various activities: Before generating tests from a model, it is helpful to use an analyzer to validate the model program, visualize its behaviors, and (optionally) perform safety and liveness analyses. An offline test generator generates test cases and expected test results from the model program, which can later be executed and checked by a test runner connected to the implementation through the test harness. This is a similar workflow to unit testing, except the test cases and expected results are generated automatically. In contrast, onthe-fly testing is quite different: the test runner generates the test case from the model as the test run is executing. On-thefly testing can execute indefinitely long nonrepeating test runs, and can accommodate nondeterminism in the implementation or its environment. To focus automated test generation on scenarios of interest, it is possible to code an optional scenario machine, a lightweight model that describes a particular scenario. The tools can combine this with the comprehensive contract model program using an operation called composition. It is also possible to code an optional strategy in order to improve test coverage according to some chosen measure. Some useful strategies are already provided. Model-based testing supports close integration of design and analysis with testing. The analyzer is similar to a model checker; it can can check safety, liveness, and temporal properties. And, the same models are used for these analyses as for automated testing. Moreover, the models are written in the same language as the implementation.