Back to the list of tutorials.
Model-Based Software Testing and Analysis with C# and NModel
Jonathan Jacky, University of Washington, USA
This tutorial teaches model-based analysis and model-based testing: methods for specifying, analyzing, and testing software, based on executable specifications called model programs.
The tutorial demonstrates the methods using a framework called NModel that is built on the C# language and .NET (the implementations which are modeled and tested do not have to be written in C#, and do not need to run in .NET). The NModel framework includes a library for writing model programs in C#, a visualization and analysis tool MPV (Model Program Viewer), a test generation tool OTG (Offline Test Generator), and a test runner tool CT (Conformance Tester) for both offline and on-the-fly testing. The library also exposes the functionality of MPV, OTG, CT and more, so you may write your own tools which are more closely adapted to your environment, or which provide other capabilities. The NModel framework, as well as .NET, are available for download at no cost.
To use this technology, you write a model program in C# that references the NModel library. Then you can use the MPV tool to visualize and analyze the behavior of your model program, in order to confirm that it behaves as you intend, and to check it for design errors. Analysis uses the same model programs and much of the same technology as testing. The MPV tool performs exploration, which generates a finite state machine (FSM) from a (possibly 'infinite') model program. By searching the FSM, MPV can perform safety analysis that checks whether the system can reach forbidden states, and liveness analysis that identifies dead states from which goals cannot be reached, including deadlocks (where the program seems to stop) and livelocks (where the program cycles endlessly without making progress). The MPV tool (and the other tools) can also form the composition of model programs by synchronizing on shared actions and interleaving unshared actions. Composition can be used for analysis: write a small scenario model program that expresses a temporal property, then compose with another model program to check it for that property.
To execute tests using the test runner CT, you write a test harness in C# that couples your implementation to the CT tool. You can use the test generator OTG to create test suites from your model program offline (in advance), or let CT generate the test on-the-fly (as the test run executes). If you wish, you can write a custom strategy in C# that CT uses to maximize coverage according to criteria you define.
In addition to teaching the fundamental skills of writing model programs, performing analyses, and generating and executing tests, the tutorial will discuss these topics:
- Finite versus 'infinite' model programs; finitizing the model program versus finitizing the analysis.
- Structuring model programs using features and composition.
- Model programs with objects; isomorphic states and isomorph elimination.
- Safety and liveness analysis by searching for states, versus composition with model programs that express temporal properties.
- Offline test generation versus on-the-fly testing.
- Controllable actions versus observable actions. The spectrum from fully controllable systems, through reactive systems (with some observable actions), to fully observable systems (such as log files or network monitors).
- Conformance criteria.
- Testing distributed systems; multiplexing and partial orders.
The tutorial will also discuss programming in the NModel framework, including these topics:
- The model program interface, for exploration under program control.
- The stepper interface, for test harnessing.
- Term representation of actions, expecially as used in test harnessing.
- The strategy interface, for guiding on-the-fly testing to achieve good coverage.
- Coverage points, a uniform way to handle coverage measures in strategies.
- Asynchronous test harness for reactive systems.