If you are developer who writes code to test software, you might want to consider using Spec Explorer. Spec Explorer is a model-based testing tool available for free through Microsoft Research that you use to model the software you're testing and create test harnesses and test case suites (http://research.microsoft.com/SpecExplorer/).

Note: Spec Explorer is available for academic use and for noncommercial evaluation. To obtain a copy, please send e-mail to seextreq@microsoft.com containing your name and affiliation. Microsoft Research will forward you a download link.

Why use a model-based test approach? There are a number of reasons. The first, and perhaps the most important reason, is using it to automate the process of creating test cases. In addition, models you create with Spec Explorer are also specifications (you'll see why further on). Thus, another reason for a model-based approach is, as the product changes, the model changes, and the spec is kept up to date.

Now, think of the old way in which you're used to writing a test harness. You come up with a list of test cases that you think will best exercise the system. You write a test harness that may make use of a common library and that calls a particular routine to exercise the code for a particular case. Naturally, you include logging so that you know what's happening in the test environment when something goes wrong. Then you run your test case and see what happens. Along the way, you may encounter product bugs that you file. By the end of test development, you have created a harness that will run a regression case or set of cases. It doesn't look for new bugs, because it isn't designed that way.

Using a model-based approach, you design a model of the software under test. What is a model? It's a description written in code of a feature under test (or a set of features) that explains exactly what conditions are expected and required for a given product behavior. It's also a graphical representation of the system under test. You can traverse this graph according to the rules of the model. Each traversal can be considered a test case. The model consists of a set of states, a set of actions (an action can be a customer behavior, for example), and the constraints on those actions. Once your model is developed, you then create an implementation of the actions in the model (we'll walk through a particular example shortly).

What about the generation of a test case or suites of tests? In my opinion, test cases are pointless in the model-based world, unless a particular path through a model finds a bug. A good model will take care of all obvious cases, and whole hosts of cases that are not so obvious. If your model finds a bug you'll want to save the case (i.e., test segment in Spec Explorer speak) for later regression tests. Spec Explorer provides you the means to do just that. However, if you're partial to owning test cases, then keep in mind that once you implement a model's actions in a test library, you have a way to generate test case suites automatically. Better yet, if you allow the model-based test harness to explore the graphical space of the model on its own, you'll find new bugs.

What about code churn? You update a model as the behavior of the software changes. It's a requirement that the model stay up to date with the software it is modeling. Therefore, you can forget about the old cases the model generated. It will generate suites of new test cases. Also, you don't have to worry so much about the spec, because you have one with the model you created in Spec Explorer, and now the spec stays up to date.

Now that you have an overview, let's focus on Spec Explorer itself. Spec Explorer evolved out of the ASML world of development. It was created with the programmer/designer in mind, so that the product details could be described with rigorous constraints. It uses Spec#, which extends the C# programming language. With Spec Explorer you create a test oracle (a set of actions and states), which is eventually bound to a specific test code implementation.

Spec Explorer's IDE
Spec Explorer comes with an IDE that looks similar to that shown in Figure 1. You'll notice that it has a Project Explorer, where you can set references to DLLs and add your specification. Additionally the Project Explorer has nodes for test suites and graphical views. In Figure 1, I've loaded a sample that comes with Spec Explorer. The sample is called "Channel" and you can find it under Program Files\Spec Explorer\samples. Spec Explorer uses a Microsoft Word plug-in so that you can write your specifications in Word.

Actions
What is an action? An action defines a customer, end user, or software behavior. Each action is made up of a function-like definition and a set of constraints. Here is an example. Suppose you have to test a Web application and in order for your customer to use it, he or she must load a Web site and then log on to it. One of the model's first actions might be called LogOn. Here's what it might look like:

[Action]
void LogOn(string userName, string password) {
     requires webApp != null;

     userLoggedOn = true;
}

The model "code" is written using the Spec# style, which is part of a built-in template if you're using Microsoft Word to create the spec (don't worry, if you don't like Word, there are other options such as plain text). Spec Explorer comes with its own compiler, so whenever you create a model (or open it), it needs to be built first. When it builds, it goes through the Word document and finds the sections in the Spec# style and compiles those, ignoring the other parts of the document.

Notice you have an attribute called "[Action]," which in Spec Explorer defines the routine as an action in the model. It has what looks like a normal function signature, plus a return value. LogOn takes a userName input parameter. It also takes a password input parameter. The LogOn action has a requirement on it: the webApp state can't be null. The requires keyword is an addition to the C# programming language provided through Spec#. It says that in order for this action to execute, the requirement must be met first.

In the action example above, the requires statement referenced a state variable, so here's a list of state variables just for this little example:

bool webApp = false;
bool userLoggedOn = false;

There are two Boolean variables defined, webApp, which tells me whether the webApp is loaded or not, and userLoggedOn, which tells me whether the user has entered user name and password and has clicked the LogOn button.

There is one more thing you should understand about actions. In the example above of LogOn, the action is controllable. Its implementation is a function that you write that actually logs on a test user. However there are other types of actions. If you have to observe an event, such as a page change in a wizard, or the appearance of a window, the action is marked as observable. A function that needs to be observable will be declared in the model like this:

[Action(Kind=ActionAttributeKind.Observable)]
bool CheckSampleEvent()

Scenarios and Actions
If you need to run a specific set of actions in a particular order, you can create scenarios. A scenario is an action that can call other actions. Normally it doesn't have a corresponding function in the class library to which the model is bound. The action that is to be a scenario must be marked as such. To mark an action as a scenario, choose Exploration Settings from the Explore menu. On the Actions tab, right-click on the action to be marked as a scenario and choose Scenario from the context menu.

So far, you have an idea of how an action is defined and how state variables are defined. Next, we'll talk briefly about Finite State Machines.