Model-Based Software Testing and Analysis with C#
Format: PDF / Kindle (mobi) / ePub
This book teaches new methods for specifying, analyzing, and testing software; essentials for creating high-quality software. These methods increase the automation in each of these steps, making them more timely, more thorough, and more effective. The authors work through several realistic case studies in-depth and detail, using a toolkit built on the C# language and the .NET framework. Readers can also apply the methods in analyzing and testing systems in many other languages and frameworks. Intended for professional software developers including testers, and for university students, this book is suitable for courses on software engineering, testing, specification, or applications of formal methods.
by events, and the controllable actions are implemented by methods called handlers. The program waits for an observable action. When one occurs, the program executes a dispatcher, code that selects a handler, and then executes the handler selected by the dispatcher. When the handler returns, the program waits again for the next observable action. We divide our control program into two classes. The Controller class is a library that contains the dispatcher and the handlers (Figures 3.2–3.4). It is
example of data abstraction. There are several ways to limit the temperature to two values. We could replace the numeric type with an enumerated type. We could even replace the single ServerSend method (where the temperature is a parameter) with two parameterless methods, each coded with one particular temperature. It is more convenient for testing if the methods and parameters are similar in the model and the implementation, so we keep the single method with its numeric parameter, but limit the
program state. In particular, use composition when the scenario can be expressed as an FSM. 7.5 Composition for analysis We now show how composition can be used for analysis. Recall that the analysis methods discussed in Chapter 6 require you to write Boolean expressions that identify unsafe states (for safety analysis) or accepting states (for liveness analysis). But sometimes it is easier to express requirements in terms of actions, rather than states. For example, in the reactive system, we
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
188.8.131.52 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. 13 P1: KNP cuny1215-book CUNY1215-Jacky 14 978 0 521 88655 0 October 2, 2007 16:18 Why We Need Model-Based Testing ✛ Temperature ✛ sensor ✲ Embedded computer (Server) ✛ commands TCP/IP network responses ✲ ✲ Data logging computer (Client) Figure 2.1. Remote instrument, a client/server system. At