In this chapter we describe two mechanisms for structuring model programs at a large scale: features and composition. Each provides a way to combine model programs in order to create a new one, or to write a model program as a collection of parts that are themselves complete (or nearly complete) model programs.

Both mechanisms are so versatile that they can be used in many ways. In Chapter 14 we use them to model interacting features. In this chapter we use them to limit analysis and testing to particular scenarios of interest. We also show how composition can be used in analysis to check temporal properties defined by sequences of actions.

Scenario control

The problem of limiting analysis and testing to particular runs of interest is called scenario control. Scenario control is necessary because we usually write a model program to act as a specification or contract, so it describes everything the implementation must do, might do, and must not do. As a result, the model program usually describes a large number of runs. When we analyze, and especially when we test, we usually do not want to consider all of these runs. We would like to limit our consideration to a particular scenario: a collection of runs (perhaps just one) that are pertinent to some issue.

Here is an example that shows why we need scenario control. Figure 7.1 shows the true FSM we obtained by exploring the client/server model program we developed in Chapter 5, Section 5.6. There are many paths through this FSM; each path describes a different run.

This chapter demonstrates why we need model-based testing, with a small but complete working example. We exhibit a software defect that is not detected by typical unit tests, but is only exposed by executing more realistic scenarios that resemble actual application program runs. We conclude that, in order to generate and check the realistic scenarios required for thorough testing, we will need more automation than is provided by the popular unit testing tools. We preview our testing techniques and show how they can detect the defect that the unit tests missed.

This chapter concerns testing methods. We also have analysis methods that can detect errors that arise during specification or design. We demonstrate an example that motivates our analysis methods in Chapter 3.

In this chapter, we also review some features of the technologies we use: the C# language, the .NET framework, and the NUnit testing tool.

Client and server

Suppose we are developing a laboratory instrument system comprising a temperature sensor connected to an embedded computer, a network, and another computer used for data storage and analysis (Figure 2.1). This is a client/server system. The server, a temperature-monitoring program, runs on the embedded computer. The client, a data-logging program, runs on the other computer. The programs communicate using the TCP/IP protocol, so the client could use the Internet to connect to a server in a remote factory or weather station.

First we start the server program Monitor by typing a command at the embedded computer:

Monitor 128.95.165.121 8023 1

The command-line arguments are the IP address and port number that the server should use, and the number of successive client connections to accept before exiting.

This chapter discusses various approaches to on-the-fly testing of closed systems. (We discuss on-the-fly testing of reactive systems in Chapter 16.)

The main difference between on-the-fly testing and offline testing is that in the case of on-the-fly testing, action sequences are not known beforehand; that is, there is no pregenerated test suite.

The use of on-the-fly testing is most relevant when the state space of the model is too large to be covered comprehensively. It may still be possible to use various finitization techniques discussed in earlier chapters to cope with this problem; on-the-fly testing is an alternative approach that may be more suitable in some situations, for example, when existence of a test suite is not relevant, or when it is not clear how to finitize or abstract the model.

Another case when on-the-fly testing is useful is when implementation under test (IUT) has hidden states that are not distinguished by the model. In other words, if a state is revisited in the model, the corresponding state in the implementation may be new. In such a case a test suite that provides transition coverage of the model might not expose an error because a transition in the model has to be traversed multiple times before the IUT is in a state where the error occurs. The error discussed in Chapter 2 is an example.

The key concept of on-the-fly testing is a strategy. Intuitively, a strategy is a function that during each step of testing selects which action to apply next.

There is a lot of research that has been done in the areas discussed in this part of the book. We mention some works that are related to the topics under discussion, and from which further related work can be found. The selection is far from exhaustive. The discussion follows the structure of this part of the book.

Compositional modeling. Protocol design and the layering principle mentioned in Section 14.1 are discussed in-depth in Comer (2000). The notion of features and the topic of feature interaction have been focused on telecommunication software. There is a series of books (see, e.g., Reiff-Marganiec and Ryan, 2005) that discuss approaches to alleviate the problem in that context. The sample protocol SP used in Section 14.2, although abstract, is related to real-life application-level network protocols such as the ones discussed in Hertel (2003).

Properties of model program composition that are discussed in Section 14.3 are analyzed formally in Veanes et al. (2007a), where composition, as treated in this book, is called parallel composition. The composition of model programs is effectively a program transformation that is most interesting when it is formally grounded in an existing semantics and has useful algebraic properties. The semantics of executing an action in a state with a rich background is founded on abstract state machines or ASMs (Gurevich, 1995; Blass and Gurevich, 2000). Determining the action traces that are produced and the properties of traces that are preserved when model programs are composed is founded on the view of model programs as labeled transition systems or LTSs (Keller, 1976; Lynch and Tuttle, 1987).

This chapter discusses testing of reactive systems. Reactive systems take inputs as well as provide outputs in the form of spontaneous reactions. The behavior of a reactive system, especially when distributed or multithreaded, can be nondeterministic. Therefore, the main difference compared to testing of closed systems is that some of the outputs of the implementation under test (IUT) may be outside the control of the tester; that is, the tester cannot predict what the exact output will be during testing. There may be multiple possible outputs and the subsequent tester inputs may depend on those outputs.

Many software systems are reactive, for example many application-level network protocols and multithreaded APIs are reactive. Such systems may produce spontaneous outputs like asynchronous events. Factors such as thread scheduling are not entirely under the control of the tester but may affect the observable behavior. In these cases, a test suite generated offline may be infeasible, since all of the observable behaviors would have to be encoded a priori as a decision tree, and the size of such a decision tree can be very large.

The main topic of this chapter is on-the-fly testing of reactive systems. The presentation of most of the material builds on on-the-fly testing of closed systems that was the topic of Chapter 12. In reactive systems, the action vocabulary is divided into controllable and observable action symbols. This terminology is tailored to match the point of view of the tester. Actions whose symbol is controllable are under the control of the tester and actions whose symbol is observable are under the control of the IUT.

Creating software is a notoriously error-prone activity. If the errors might have serious consequences, we must check the product in some systematic way. Every project uses testing: check the code by executing it. Some projects also inspect code, or use static analysis tools to check code without executing it. Finding the best balance among these assurance methods, and the best techniques and tools for each, is an active area of research and controversy. Each approach has its own strengths and weaknesses.

The unique strength of testing arises because it actually executes the code in an environment similar to where it will be used, so it checks all of the assumptions that the developers made about the operating environment and the development tools.

But testing is always incomplete, so we have to use other assurance methods also. And there are other important development products besides code. To be sure that the code solves the right problem, we must have a specification that describes what we want the program to do. To be sure that the units of code will work together, we need a design that describes how the program is built up from parts and how the parts communicate. If the specification or design turns out to be wrong, code may have to be reworked or discarded, so many projects conduct reviews or inspections where people examine specifications and designs. These are usually expressed in informal notations such as natural language and hand-drawn diagrams that cannot be analyzed automatically, so reviews and inspections are time-consuming, subjective, and fallible.

This chapter demonstrates why we need model-based analysis. We exhibit a program with design errors that cause safety violations (where the program reaches forbidden states), deadlocks (where the program seems to stop running and stops responding to events), and livelocks (where the program cycles endlessly but can't make progress). We preview our analysis and visualization techniques and show how they can reveal the design errors, even before beginning any testing.

Reactive system

Suppose we are developing a process control program that runs on an embedded computer connected to sensors, timers, and a supervisor program (Figure 3.1). The temperature monitor discussed in Chapter 2 could be a component of this system; here we consider a higher level of integration. This is a reactive system that responds to events in its environment. In this chapter we consider just one of its features: the temperature-calibration factor. The controlled process depends on the temperature. In order to control the process accurately, the control program must obtain a temperature reading from a sensor and use it to compute the calibration factor. The calibration factor is then used in subsequent process control computations (which we do not discuss here).

The temperature in the process can change continuously, so the control program must sample the temperature often. The control program frequently polls the sensor (requests a sample). The sensor usually responds with a message that contains the most recently measured temperature. We distinguish controllable actions that the program commands from observable actions that originate in the attached equipment. All that the program can do in regard to observable actions is to wait for them (and observe them).

This book teaches new methods for specifying, analyzing, and testing software. They are examples of model-based analysis and model-based testing, which use a model that describes how the program is supposed to behave. The methods provide novel solutions to the problems of expressing and analyzing specifications and designs, generating test cases, and checking the results of test runs. The methods increase the automation in each of these activities, so they can be more timely, more thorough, and (we expect) more effective. The methods integrate concepts that have been investigated in academic and industrial research laboratories for many years and apply them on an industrial scale to commercial software development. Particular attention has been devoted to making these methods acceptable to working software developers. They are based on a familiar programming language, are supported by a well-engineered technology, and have a gentle learning curve.

These methods provide more test automation than do most currently popular testing tools, which only automate test execution and reporting, but still require the tester to code every test case and also to code an oracle to check the results of every test case. Moreover, our methods can sometimes achieve better coverage in less testing time than do hand-coded tests.

Testing (i.e., executing code) is not the only assurance method. Some software failures are caused by deep errors that originate in specifications or designs. Model programs can represent specifications and designs, and our methods can expose problems in them. They can help you visualize aspects of system behavior.

In this chapter we introduce model-based testing. We test the client/server implementation we described in Chapter 2, and reveal the defect we discussed there. We generate the test suite and check the results with the model program we developed in Chapter 5, Section 5.6. We introduce our test generator tool otg and our test runner tool ct, and show how to write a test harness that connects an implementation to the ct tool.

In this chapter we describe offline test generation, where test suites are generated before running the tests. Offline test generation works best with finite model programs that can be explored completely. In Chapter 12 we introduce on-the-fly testing, where the test case is generated as the test executes. On-the-fly testing is an attractive alternative for “infinite” model programs that cannot be explored completely.

In this chapter we test closed systems where the tester controls every action. In Chapter 16 we test reactive systems, where some actions are invoked by the environment.

Offline test generation

The offline test generator otg explores a model program to create a finite state machine (FSM), traverses paths through the FSM, and saves the paths in a file so they can be used later. The paths define a collection of program runs. The collection is called a test suite; each run in the collection is a test case. Later, the implementation can execute the test suite, under the control of a test runner.

This chapter introduces model programs. We show how to code model programs that work with the tools, by using attributes from the modeling library along with some coding conventions.

In this chaper we also explain the process of writing a model program: the steps you must go through to understand the implementation and design the model program. Writing a model program does not mean writing the implementation twice. By focusing on the purpose of the model, you can write a model program that is much smaller and simpler than the implementation, but still expresses the features you want to test or analyze.

Here in Part II, we explain modeling, analysis, and testing with finite model programs that can be analyzed exhaustively (completely). The programs and systems we model here are “infinite” – perhaps not mathematically infinite, but too large to analyze exhaustively. One of the themes of this chapter is how to finitize (make finite) the model of an “infinite” system. Starting in Part III, the model programs are also “infinite”; we finitize the analysis instead.

In this chapter we develop and explain three model programs: a newsreader user interface, the client/server system of Chapter 2, and the reactive system of Chapter 3. We will perform safety and liveness analyses of the reactive system model in Chapter 6. We will generate and check tests of the implementation using the client/server model in Chapter 8.

We have seen many different uses of composition in the previous chapters. In this chapter we are going to take a closer look at the use of composition as a general modeling technique to break down larger models into smaller models.

We are going to look at an example that illustrates how this technique can be applied to real-life complex application-level network protocols. Such protocols are abundant. Modern software architectures rely heavily on the fact that two parties that need to communicate, for example a client and a server, or two servers, do so by using a well-defined (application-level network) protocol.

We then discuss some of the main properties of model program composition and provide a summary of the various uses of model program composition.

Modeling protocol features

A real-life protocol can be intrinsically complex. There are several reasons for this. A protocol typically has multiple layers and depends on or uses other protocols. In a good protocol design, internal details of the underlying protocols should not leak out and the layering principle should be maintained. Another reason is that a protocol typically includes many different features within a single layer. Intuitively, a feature is a part or an aspect of the overall functionality of the protocol. Features interact and together define the protocol as a whole.

An important property of protocols is that enough information is present in messages, usually in message headers, so that it is possible to maintain a consistent view of the state of the protocol on both sides of the protocol users.