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.

There are many modeling languages based on guarded update rules (or something similar), including Alloy (Jackson, 2006), ASMs (Gurevich, 1995; Börger and Stärk, 2003), B (Abrial, 1996), Promela (Holzmann, 2004), TLA (Lamport, 2002), Unity (Chandy and Misra, 1988), VDM (Fitzgerald and Larsen, 1998), and Z (Woodcock and Loomes, 1989; Spivey, 1992; Davies and Woodcock, 1996; Jacky, 1997). Case studies in these languages show how different kinds of systems can be described in modeling styles similar to ours.

The immediate predecessors of the modeling library and tools described in this book are the AsmL language and the AsmL-T tool (Barnett et al., 2003), and more recently, the SpeC# language and the Spec Explorer tool (Veanes et al., in press; Campbell et al., 2005a). Development on Spec Explorer continues.

Peled (2001) presents an exhaustive exploration algorithm similar to ours. Grieskamp et al. (2002) describe a more complex exploration algorithm.

Exploration has some similarities to model checking, which also generates and explores a finite state machine (FSM), but usually emphasizes verifying (or providing counterexamples to) properties expressed as formulas in temporal logic. This is similar to our checking of temporal properties, but we express them with FSMs instead of formulas. Model checking was originally described by Clarke et al. (1986) in a classic paper and later described in a survey article (Clarke et al., 1994) and a book (Clarke et al., 1999). Some other model checkers are described in the books by Peled (2001) and Holzmann (2004).

Composition of model programs is a generalization of the construction of finite automata for the intersection of regular languages. For example, see the discussion following Theorem 3.3 on pp. 59–60 of Hopcroft and Ullman (1979).

In this chapter we introduce exploration our primary technique for analyzing model programs. Exploration generates a finite state machine (FSM) from a model program. The FSM can then be used for visualization, analysis, and offline lest generation.

In this chapter we show how model-based analysis reveals the design errors in the reactive system we discussed in Chapter 3, by exploring the model program we developed in Chapter 5, Section 5.7. We explain and demonstrate safety analysis that identifies unsafe (forbidden) states and liveness analysis that identifies dead states from which goals cannot be reached. Dead states indicate deadlocks (where the program seems to stop running and stops responding to events) or livelocks (where the program keeps running but can't make progress).

In this chapter we also introduce the mpv (Model Program Viewer) tool for visualization and analysis, and explain how to use the modeling library features that support analysis.

Finite state machines

In this section we motivate and explain FSMs.

Simulation is the most limited and labor-intensive model-based analysis technique because it only considers one run at a time (Chapter 5, Section 5.5). To perform more thorough analyses – to detect the design errors discussed in Chapter 3, for example – we need to consider many different runs. The obvious way would be to code a large number of runs, but this is not a practical solution. In order to get good coverage of program behaviors, we would usually have code a great many runs, and some would be very long. But the collection of runs would be redundant. The same sequences of actions would appear again and again in different runs, and even within a single run.

Strings are common to most computer programs. Certain types of programs, such as word processors and web applications, make heavy use of strings, which forces the programmer of such applications to pay special attention to the efficiency of string processing. In this chapter, we examine how C# works with strings, how to use the String class, and finally, how to work with the StringBuilder class. The StringBuilder class is used when a program must make many changes to a String object because strings and String objects are immutable, whereas StringBuilder objects are mutable. We'll explain all this later in the chapter.

WORKING WITH THE STRING CLASS

A string is a series of characters that can include letters, numbers, and other symbols. String literals are created in C# by enclosing a series of characters within a set of double quotation marks. Here are some examples of string literals:

1. “David Ruff”

2. “the quick brown fox jumped over the lazy dog”

3. “123-45-6789”

4. “[email protected]”

A string can consist of any character that is part of the Unicode character set. A string can also consist of no characters. This is a special string called the empty string and it is shown by placing two double quotation marks next to each other (“ ”). Please keep in mind that this is not the string that represents a space. That string looks like this—“ ”.

The study of networks has become one of the great scientific hotbeds of this new century, though mathematicians and others have been studying networks for many hundreds of years. Recent developments in computer technology (i.e., the Internet), and in social theory (the social network, popularly conceived in the concept of “six degrees of separation”), have put a spotlight on the study of networks.

In this chapter, we look at how networks are modeled with graphs. We're not talking about the graphs such as pie graphs or bar graphs. We define what a graph is, how they're represented in VB.NET, and how to implement important graph algorithms. We also discuss the importance of picking the correct data representation when working with graphs, since the efficiency of graph algorithms is dependent on the data structure used.

GRAPH DEFINITIONS

A graph consists of a set of vertices and a set of edges. Think of a map of your state. Each town is connected with other towns via some type of road. A map is a type of graph. Each town is a vertex and a road that connects two towns is an edge. Edges are specified as a pair, (v1, v2), where v1 and v2 are two vertices in the graph. A vertex can also have a weight, sometimes also called a cost.

A dictionary is a data structure that stores data as a key–value pair. The DictionaryBase class is used as an abstract class to implement different data structures that all store data as key–value pairs. These data structures can be hash tables, linked lists, or some other data structure type. In this chapter, we examine how to create basic dictionaries and how to use the inherited methods of the DictionaryBase class. We will use these techniques later when we explore more specialized data structures.

One example of a dictionary-based data structure is the SortedList. This class stores key–value pairs in sorted order based on the key. It is an interesting data structure because you can also access the values stored in the structure by referring to the value's index position in the data structure, which makes the structure behave somewhat like an array. We examine the behavior of the SortedList class at the end of the chapter.

THE DICTIONARYBASE CLASS

You can think of a dictionary data structure as a computerized word dictionary. The word you are looking up is the key, and the definition of the word is the value. The DictionaryBase class is an abstract (MustInherit) class that is used as a basis for specialized dictionary implementations.

Trees are a very common data structure in computer science. A tree is a nonlinear data structure that is used to store data in a hierarchical manner. We examine one primary tree structure in this chapter, the binary tree, along with one implementation of the binary tree, the binary search tree. Binary trees are often chosen over more fundamental structures, such as arrays and linked lists, because you can search a binary tree quickly (as opposed to a linked list) and you can quickly insert data and delete data from a binary tree (as opposed to an array).

THE DEFINITION OF A TREE

Before we examine the structure and behavior of the binary tree, we need to define what we mean by a tree. A tree is a set of nodes connected by edges. An example of a tree is a company's organization chart (see Figure 12.1).

The purpose of an organization chart is to communicate to the viewer the structure of the organization. In Figure 12.1, each box is a node and the lines connecting the boxes are the edges. The nodes, obviously, represent the entities (people) that make up an organization. The edges represent the relationship between the entities. For example, the Chief Information Officer (CIO), reports directly to the CEO, so there is an edge between these two nodes. The IT manager reports to the CIO so there is an edge connecting them.

The study of data structures and algorithms is critical to the development of the professional programmer. There are many, many books written on data structures and algorithms, but these books are usually written as college textbooks and are written using the programming languages typically taught in college—Java or C++. C# is becoming a very popular language and this book provides the C# programmer with the opportunity to study fundamental data structures and algorithms.

C# exists in a very rich development environment called the .NET Framework. Included in the .NET Framework library is a set of data structure classes (also called collection classes), which range from the Array, ArrayList, and Collection classes to the Stack and Queue classes and to the HashTable and the SortedList classes. The data structures and algorithms student can now see how to use a data structure before learning how to implement it. Previously, an instructor had to discuss the concept of, say, a stack, abstractly until the complete data structure was constructed. Instructors can now show students how to use a stack to perform some computation, such as number base conversions, demonstrating the utility of the data structure immediately. With this background, the student can then go back and learn the fundamentals of the data structure (or algorithm) and even build their own implementation.