The calculation of the date of Easter has a fascinating history, and algorithms and computer programs abound (for example, [1], [2], [9], [10], [13], and [14]). Many of the computations rely on the formulas of Gauss [5], [6] (see also [8]). Our fixed-date approach allows considerable simplification of “classical” algorithms.

The history of the establishment of the date of Easter is long and complex; good discussions can be found in [3] and [7]. The Council of Nicsa convened in 325 C.E. by Constantine the Great, was concerned with uniformity across various Christian groups. At the time of Nicæa, almost everyone in the official Church agreed to the definition that Easter was the first Sunday after the first full moon occurring on or after the vernal equinox [3] (a rule promulgated by Dionysius Exiguus and the Venerable Bede, who attributed it to the Council of Nicæa).

Structure

The Bahá'í (or Badī') calendar begins its years on the day of the vernal equinox. Theoretically, if the actual time of the equinox occurs after sunset, then the year should begin a day later [2]. Current practice in the West, however, is to begin on March 21 of the Gregorian calendar, regardless. The theoretical, astronomical version of the Bahá'í calendar is described in Section 15.3. The calendar is based on the 19-year cycle 1844–1863 of the Bāb, the martyred forerunner of Baha'u'llāh and co-founder of the Bahá'í faith.

As in the Islamic calendar, days are from sunset to sunset. Unlike the Islamic calendar, years are solar; they are composed of 19 months of 19 days each with an additional period of 4 or 5 days after the eighteenth month. Leap years in the West follow the same pattern as in the Gregorian calendar.

The concepts presented in this book are based on ideas from mathematics and theoretical computer science. Readers certainly do not need to understand these theoretical aspects in order to use the techniques we present. However, some may be interested in pursuing these topics in further detail, and for these readers we can point to the following sources of information.

The central idea of a model program that we present throughout the book is based on the theory of abstract state machines (ASMs) conceived by Yuri Gurevich in 1980s. An ASM is a formal way to describe the steps of an algorithm. It gives a mathematical view of program state (including the state of object-oriented systems and systems with complex structure). There is a well-developed body of scientific literature on the topic. Readers interested in ASMs may wish to see the ASM Web page maintained at the University of Michigan (ASM, 2006). Of particular interest is the “Lipari guide” (Gurevich, 1995).

We also use ideas taken from finite automata, mathematical logic, and set theory. The composition of automata for language intersection is a core concept. A classic text that describes finite automata and their properties is Hopcroft and Ullman (1979). A useful and practical introduction to logic and set theory is found in Lipschutz (1998).

A mathematically rigorous survey of assurance methods including modeling, testing, and static analysis appears in the book by Peled (2001).

The ideas in this book were developed and made practical at Microsoft Research from 1999 through 2006 in the Foundations of Software Engineering group (FSE, 2006).

There are many existing formal methods that support modeling and analysis with complex state, 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 methods demonstrate many ways to use sets, bags, sequences, maps, and other data types similar to the ones in the modeling library.

AsmL (abstract state machine language) (Gurevich et al., 2005) includes highlevel data structures like sets and maps and builds on the theory of partial updates (Gurevich and Tillmann, 2005) that allows pointwise changes to such data structures that may, moreover, be nested. AsmL was first supported in the model-based testing tool AsmL-T (Barnett et al., 2003) and is also supported in the Spec Explorer tool (Spec Explorer, 2006). Spec Explorer also supports an extension of the SpeC# language (Barnett et al., 2005) with high-level data structures such as sets and maps.

The pruning techniques discussed in Section 11.2 are mostly based on work that was done in Spec Explorer (Veanes et al., in press). The use of composition in this context is based on Veanes et al. (2007a). The state grouping technique discussed in Section 11.2.5 is introduced in Grieskamp et al. (2002). The algorithm is also explained in Börger and Stärk (2003, Section 3.2). The technique can be extended to multiple groupings (Campbell and Veanes, 2005) that can be used to define groupings per feature in a model program with multiple features. State grouping is related to abstraction in model checking (Clarke et al., 1999).

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).