June 26-29 2007, Tallinn, Estonia

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:

The tutorial will also discuss programming in the NModel framework, including these topics: