Model-Based Testing of Reactive Systems

Abstract

Testing is the primary hardware and software verification technique used by industry today. Usually, it is ad hoc, error prone, and very expensive. In recent years, however, many attempts have been made to develop more sophisticated, formal testing methods. But a comprehensive account of the area of formal testing is missing. The goal of this seminar volume is to provide an in-depth exposure of this emerging area, especially to make it easily accessible to new researchers in this field. Since testing describes the methodology used to obtain better systems, it is widely used in many scientific and industrial sectors dealing with system de- velopment. As such, a book on testing is hardly ever a comprehensive overview on the whole domain of testing, but a selection of important approaches and application domains. In this volume, we focus on testing methods for reactive systems. By reactive systems, we understand software and hardware systems with a (usually) non-terminating behavior that interact through visible events, such as Web servers, communication protocols, operating systems, smart cards, processors, etc. Furthermore, in most chapters of this book, we follow the so-called model- based approach. The underlying assumption in the model-based approach is the existence of a precise formal model of the system being developed. This model can be used for studying the system to be. Especially in the testing phase of product development, it can be used to generate complete test suites to show conformance of the model and the actual implementation, or, just to derive “interesting” test cases to check the developed system. The 19 chapters of the book are grouped into six parts. In the first part, we present the approaches for testing for finite-state machines, also called Mealy machines. The second part, called testing of labeled transition systems, gives an overview of the testing theory due to Hennessy and De Nicola together with its extensions to I/O, timed, and probabilistic systems. In Part III, we focus on methodology, algorithms, and techniques for model-based test case generation. The methods illustrated in the first three parts of the book led to the de- velopment of test tools and have been applied in many case studies showing their advantages and drawbacks. Several tools and case studies are presented in Part IV. While test case generation can be considered the heart of testing, the testing process as a whole is more complicated. The test cases have to executed on the system under test. In several application domains, test suites are used to show conformance to a standard. For this, test cases have to be interchanged among developers. Furthermore, testing should be included in the overall development process. In Part V, called Standardized Test Notation and Execution Architecture we cover recent developments.