nach oben

2005 | Buch

Kapitel lesen Erstes Kapitel lesen

Model-Based Testing of Reactive Systems

Advanced Lectures

herausgegeben von: Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

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. This coherent book provides an in-depth assessment of this emerging field, focusing on formal testing of reactive systems.

This book is based on a seminar held in Dagstuhl Castle, Germany, in January 2004. It presents 19 carefully reviewed and revised lectures given at the seminar in a well-balanced way ensuring competent complementary coverage of all relevant aspects. An appendix provides a glossary for model-based testing and basics on finite state machines and on labelled transition systems. The lectures are presented in topical sections on testing of finite state machines, testing of labelled transition systems, model-based test case generation, tools and case studies, standardized test notation and execution architectures, and beyond testing.

Inhaltsverzeichnis

Frontmatter

Testing of Finite State Machines

Part I. Testing of Finite State Machines

Abstract

The first part of the book is devoted to the problem of black-box testing of finite state machines in order to discover properties of their behavior and to check that they conform to given specifications.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

1 Homing and Synchronizing Sequences

Abstract

This chapter considers two fundamental problems for Mealy machines, i.e., finite-state machines with inputs and outputs. The machines will be used in subsequent chapters as models of a system or program to test. We repeat Definition 21.1 of Chapter 21 here: readers already familiar with Mealy machines can safely skip to Section 1.1.2.

Sven Sandberg

2 State Identification

Abstract

In this chapter, we deal with the problem of state identification of finite-state Mealy machines. Before defining the problem formally, let us illustrate it with a few examples and point out its differences with the similar problem of finding a homing sequence.

Moez Krichen

3 State Verification

Abstract

State verification is a more restricted problem than state identification, discussed in Chapter 2. As in state verification, we know the state diagram of the system under test. The difference is that we have an assumption about which state the system is currently in, and the objective is to check that this assumption is correct. The basic idea is that when testing a machine, we can give it an input sequence, and then use state verification to verify that the sequence took the machine under test to the expected state.

Henrik Björklund

4 Conformance Testing

Abstract

In this chapter we tackle the problem of conformance testing between finite state machines. The problem can be briefly described as follows [LY96]. Given a finite state machine M _S which acts as specification and for which we know its transition diagram, and another finite state machine M _I which is the alleged implementation and for which we can only observe its behavior, we want to test whether M _I correctly implements or conforms to M _S. The problem of conformance testing is also called fault detection, because we are interested in uncovering where M _I fails to implement M _S, or machine verification in the circuits and switching systems literature.

Angelo Gargantini

Part II. Testing of Labeled Transition Systems

Abstract

This part of the book is concerned with the theory of model-based testing where real systems are assumed to be modeled as labeled transition systems (and extensions thereof). Labeled transition systems were proposed by Keller [Kel76] and are widely used as underlying models for data-intensive systems (sequential and concurrent programs) as well as hardware circuits. The starting point of this form of model-based testing is a precise, unambiguous model description of the system under test. Based on this formal specification, test generation algorithms generate provably valid tests, i.e., tests that test what should be tested and no more than that. These algorithms provide automatic, faster and less error-prone test generation facilities. A sketch of the testing approach is given in Figure 9.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Testing of Labeled Transition Systems

5 Preorder Relations

Abstract

The usefulness of formalisms for the description and the analysis of reactive systems is closely related to the underlying notion of behavioral equivalence. Such an equivalence should formally identify behaviors that are informally indistinguishable from each other, and at the same time distinguish between behaviors that are informally different.

Stefan D. Bruda

6 Test Generation Algorithms Based on Preorder Relations

Abstract

Testing theory has been studied for a long time. Based on finite state machines at the beginning, it has been extended to conformance testing of transition systems. Test generation methods have been developed for both of these models.

Valéry Tschaen

7 I/O-automata Based Testing

Abstract

The testing theories on labeled transition systems, that we have seen so far, abstract from input and output actions. They only use the general concept “action” without a notion of direction. Although theoretically appealing, this may seem strange from a practical perspective. As a tester, we stimulate the system under test by providing inputs and observe its responses; the outputs of the system under test.

Machiel van der Bijl, Fabien Peureux

8 Test Derivation from Timed Automata

Abstract

A real-time system is a discrete system whose state changes occur in real-numbered time [AH97]. For testing real-time systems, specification languages must be extended with constructs for expressing real-time constraints, the implementation relation must be generalized to consider the temporal dimension, and the data structures and algorithms used to generate tests must be revised to operate on a potentially infinite set of states.

Laura Brandán Briones, Mathias Röhl

9 Testing Theory for Probabilistic Systems

Abstract

The aim of this chapter is to give a survey of testing relations for probabilistic systems. We summarize the relevant material on probabilistic extensions of the work of De Nicola and Hennessy [dNH84] who defined implementation relations for nondeterministic processes based on a notion of testing (see also Chapter 5). We mainly concentrate on the relative expressive power of the different preorders. All presented relations are primarily of theoretical interest and to the best of our knowledge their usefulness in practical applications has not been shown yet.

Verena Wolf

Part III. Model-Based Test Case Generation

Abstract

The previous parts of this book have, in general, been concerned with checking models against models. A theoretical underpinning with, among other things, respect to completeness of these approaches has been given.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Model-Based Test Case Generation

10 Methodological Issues in Model-Based Testing

Abstract

Testing denotes a set of activities that aim at showing that actual and intended behaviors of a system differ, or at increasing confidence that they do not differ. Often enough, the intended behavior is defined by means of rather informal and incomplete requirement specifications. Test engineers use these specification documents to gain an approximate understanding of the intended behavior. That is to say, they build a mental model of the system. This mental model is then used to derive test cases for the implementation, or system under test (SUT): input and expected output. Obviously, this approach is implicit, unstructured, not motivated in its details and not reproducible.

Alexander Pretschner, Jan Philipps

11 Evaluating Coverage Based Testing

Abstract

In the previous chapters, various formal testing theories have been discussed. The correctness of an implementation with respect to a model is denoted by a so-called conformance relation. Conformance relations are relations between mathematical abstractions of implementations and models. Based on these conformance relations, different testing strategies have been defined. In this chapter, we concentrate on formal objects used to select test suites. These formal objects are so-called coverage criteria. A coverage criterion is a property that a selected test suite has to satisfy. We explore to which purposes these coverage criteria can be used for. Then we concentrate on the fault detection ability of a test suite satisfying a given coverage criterion.

Christophe Gaston, Dirk Seifert

12 Technology of Test-Case Generation

Abstract

Model based test case generation deals with the generation of test cases based on test case specifications and a model of the system under test (SUT). Since the number of possible test cases is in general too large to be practically useful, test case specifications are used to select interesting test cases. Therefore, test case generation can be seen as the search problem of finding appropriate test cases. In the previous chapter, several kinds of test case specifications, in particular coverage criteria, have been presented. In the current chapter, we will show how techniques from various fields in computer science such as program analysis and formal methods can be applied to generate test cases that satisfy such specifications. The input part of each test case can then be fed into the SUT whose output is compared with the output part of the test case in order to detect errors. In particular, we will cover test case generation by theorem proving, symbolic execution, and model checking. Although these techniques are often used in combination, we will describe them separately in order to show their applicability and specific features from different points of view.

Levi Lúcio, Marko Samer

13 Real-Time and Hybrid Systems Testing

Abstract

Real-Time and Hybrid Systems A system whose functionality is not only dependent on the logical results of computation but also on the time in which this computation takes place is called real-time system. We speak of hard real-time if timing constraints always have to be met exactly. In contrast, soft real-time allows lateness under specified conditions.

Kirsten Berkenkötter, Raimund Kirner

Part IV. Tools and Case Studies

Abstract

The previous parts of this book have shown how to relate models to models, and how to relate models to actual systems running in their actual environments. This included the theoretical background as well as pragmatic and technological considerations when it came to reducing the number of test cases to a “sufficient” number.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Tools and Case Studies

14 Tools for Test Case Generation

Abstract

The preceding parts of this book have mainly dealt with test theory, aimed at improving the practical techniques which are applied by testers to enhance the quality of soft- and hardware systems. Only if these academic results can be efficiently and successfully transferred back to practice, they were worth the effort.

Axel Belinfante, Lars Frantzen, Christian Schallhart

15 Case Studies

Abstract

In this chapter, we review and analyze some of the significant case studies published on the application of model-based testing. We focus on case studies done in industrial contexts in order to evaluate how model-based testing is applied in practice and how far it is applied. But we also review a few proof of concept and benchmarking case studies. We review case studies on model-based testing of processors [DBG01, SA99, FKL99], smart cards [PPS+03, CJRZ01], protocols [KVZ98, BFdV+99], Java and POSIX [FHP02]. This list is not exhaustive; but it is a good representation of the range of applications, methods and tools used in the available model-based testing case studies. There could be other case studies which we did not detect or have been published recently.

Wolfgang Prenninger, Mohammad El-Ramly, Marc Horstmann

Part V. Standardized Test Notation and Execution Architecture

Abstract

The previous parts of this volume dealt mainly with test case generation. We have presented methods or finite-state machines and for transition systems and reviewed tools and case studies. In this part, we give two examples for formal test notations. While the two description methods have been designed for specifying test cases manually, it is in general possible to use these notations also for automatically generated test cases, which gives the link to the previous parts.

Chapter 16 gives an introduction to TTCN-3, the Testing and Test Control Notation, which is a standardized language to formulate tests and to control their execution.

In Chapter 17, the standardized UML 2.0 test profile is explained. It provides means to use UML both for system modelling as well as test case specification.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Standardized Test Notation and Execution Architecture

16 TTCN-3

Abstract

This chapter presents TTCN-3, the Testing and Test Control Notation, which is the most used technology in the protocol testing field. Many of the previous chapters concern the problem of how to create tests for a system we want to test. In this chapter we consider the problem of test execution. Test execution comprises the following activities: test data is applied to a SUT, the behavior of the SUT is monitored, and expected and actual behaviors are compared in order to yield a verdict.

George Din

17 UML 2.0 Testing Profile

Abstract

The Unified Modeling Language (UML) is a visual language to support the design and development of complex object-oriented systems [RJB99]. While UML models focus primarily on the definition of system structure and behavior, they provide only limited means for describing test objectives and test procedures. In 2001, a consortium was built by the Object Management Group (OMG) in order to develop a UML 2.0 profile for the testing domain [OMG02, UMLa].

Zhen Ru Dai

Part VI. Beyond Testing

Abstract

This last part of the book introduces two extensions of the typical testing approach. It describes methods for the continuous testing effort, also at a later run-time of the system. Furthermore, it recalls essentials of model checking, a different powerful technique to get “better” systems, on the one hand to separate model checking and testing, on the other hand, to show possible combinations leading to approaches like black box checking or adaptive model checking. The latter glue learning of automata and model checking to study an underlying system.

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Beyond Testing

18 Run-Time Verification

Abstract

We are going into a ubiquitous computing world, where computation is in every object around us. When that finally happens, when computers finally “disappear into the woodwork” [Dav02], more people will be using computers without realizing they are interacting with computers. This is beginning to happen now. Once people are surrounded by computational artifacts, and when these artifacts are linked together by all forms of networking, both wired and wireless, then the current incipient computer utility will become the predominant aspect.

Séverine Colin, Leonardo Mariani

19 Model Checking

Abstract

When developing hard- or software systems one starts with a collection of requirements. Most requirements arise due to the needs of the customer, others originate from design decisions and further constraints. Of course, the final system should fulfill these requirements. Besides general requirements like scalability and performance, there is often a large number of formal requirements which concern the functionality of the system. Typical requirements of this kind are lifeness requirements (e.g. bad things never happen), fairness requirements (e.g. the system continues doing meaningful things), and in general requirements which prescribe the chronological order of events (e.g. event A may only occur after event B).

Therese Berg, Harald Raffelt

Part VII. Appendices

Abstract

20 Model-Based Testing – A Glossary

21 Finite State Machines

22 Labelled Transition Systems

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner

Appendices

20 Model-Based Testing – A Glossary

Abstract

The idea of model-based testing is to compare the I/O behavior of a valid behavior model to that of a system one wants to test (the system under test, SUT). In order to do so, a few I/O traces of the model are fixed. Picking “interesting” traces is a demanding task, and it is reflected in test purposes and test case specifications. The input part of a test case is applied to the SUT, and the output of the SUT is compared to the output of the model (this expected output is part of the test case).

Alexander Pretschner, Martin Leucker

21 Finite State Machines

Abstract

In this appendix, we review basic definitions and the Mealy machine model. The definitions and most of the notation follow [LY94, LY96].

Bengt Jonsson

22 Labelled Transition Systems

Abstract

Let Act be a countable set of actions ranged over by a, b, c, .... Action τ denotes the distinguished invisible (or, unobservable) action, i.e., \(\tau \not\in\) Act.

Joost-Pieter Katoen

Backmatter

Titel: Model-Based Testing of Reactive Systems
herausgegeben von: Manfred Broy
Bengt Jonsson
Joost-Pieter Katoen
Martin Leucker
Alexander Pretschner
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-32037-1
Print ISBN: 978-3-540-26278-7
DOI: https://doi.org/10.1007/b137241

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Testing of Finite State Machines

Part I. Testing of Finite State Machines

1 Homing and Synchronizing Sequences

2 State Identification

3 State Verification

4 Conformance Testing

Part II. Testing of Labeled Transition Systems

Testing of Labeled Transition Systems

5 Preorder Relations

6 Test Generation Algorithms Based on Preorder Relations

7 I/O-automata Based Testing

8 Test Derivation from Timed Automata

9 Testing Theory for Probabilistic Systems

Part III. Model-Based Test Case Generation

Model-Based Test Case Generation

10 Methodological Issues in Model-Based Testing

11 Evaluating Coverage Based Testing

12 Technology of Test-Case Generation

13 Real-Time and Hybrid Systems Testing

Part IV. Tools and Case Studies

Tools and Case Studies

14 Tools for Test Case Generation

15 Case Studies

Part V. Standardized Test Notation and Execution Architecture

Standardized Test Notation and Execution Architecture

16 TTCN-3

17 UML 2.0 Testing Profile

Part VI. Beyond Testing

Beyond Testing

18 Run-Time Verification

19 Model Checking

Part VII. Appendices

Appendices

20 Model-Based Testing – A Glossary

21 Finite State Machines

22 Labelled Transition Systems

Backmatter

Premium Partner