Testing of Reactive Systems, Summer Term 2009
Type | Time | Place | Start | Lecturer |
V/Ü | Mon 12:30--14:00 | Room 4210 | 20. April 2009 | |
V/Ü | Tue 11:45 -- 13:15 | Room 4210 |
Note: The lecture is V3, the exercises Ü1. The exercises will be held bi-weekly in one of the two lecture slots. The first lecture will be held Monday, 20. April, in AH 3. On the schedule you can also find the material, as it will be given out.
News
17 July 2009 | There will be no new exercise sheet. The last part of the script is available. The complete script in one file is also available. |
6 July 2009 | Exercise 5 is online. |
29 June 2009 | Chapter 5 and part of Chapter 6 of the script are on-line. Note that Section5.5 is not relevant. |
22 June 2009 | Exercise 4 is online. |
10 June 2009 | The first part of Chapter 5 of the script is on-line. |
8 June 2009 | Exercise 3 is online. |
26 May 2009 | Homework for lectures on June 9 and June 15: read Section 4.8 in the script on compositionality of ioco. |
26 May 2009 | The script with the rest of chapter 4 is online. |
17 May 2009 | Exercise 2 is online. |
17 May 2009 | The script up to Section 4.5 is online. I ask to read Chapter 4, up to and including Section 4.4. This will be the material for the lecture on Tuesday, 19 May. |
17 May 2009 | Important: The small audience allows to organise the lecture and exercises in a different way. The lecture will now place in my office (Room 4210) in Building E1. I ask to read certain sections of the script before the lectures. I will announce here how far we should be able to go. |
21.Apr 2009 | Slides and Script for first two lectures are online. See schedule. |
24 Feb 2009 | Here we are! |
Schedule
...where you can find the material of the course, as it is released.
Contents
Testing is one of the most natural approaches to find out about the
behavior of systems, be it Java classes, UNIX processes, or protocol
components. It is the primary tool to find bugs in implemented
systems, and it is used by everybody who is concerned with software
development.
However, manual, ad-hoc testing is time-consuming, error-prone, and
most of all, boring. In industrial settings, test-automation goes only
as far as automatic test-execution (if that), however, test-cases are
written mostly manually. Especially for reactive systems, which show
nondeterministic behavior due to concurrent execution, obtaining
test-suits with a satisfying coverage is a time consuming and thus
expensive task. Moreover, it has to be repeated and repeated again as
the system-under-test develops and mutates. Automatic test-case
generation is thus most desirable.
The primary target of this lecture is to introduce into the
specification-based approach of testing. In this approach, a system to
be tested is described as a formal model, and this model is used to
derive test-cases automatically. In order to come to this point, the
necessary theoretical groundwork is laid.
The approach is a formal one, rooted in automata theory.
The following issues are addressed:
behavior of systems, be it Java classes, UNIX processes, or protocol
components. It is the primary tool to find bugs in implemented
systems, and it is used by everybody who is concerned with software
development.
However, manual, ad-hoc testing is time-consuming, error-prone, and
most of all, boring. In industrial settings, test-automation goes only
as far as automatic test-execution (if that), however, test-cases are
written mostly manually. Especially for reactive systems, which show
nondeterministic behavior due to concurrent execution, obtaining
test-suits with a satisfying coverage is a time consuming and thus
expensive task. Moreover, it has to be repeated and repeated again as
the system-under-test develops and mutates. Automatic test-case
generation is thus most desirable.
The primary target of this lecture is to introduce into the
specification-based approach of testing. In this approach, a system to
be tested is described as a formal model, and this model is used to
derive test-cases automatically. In order to come to this point, the
necessary theoretical groundwork is laid.
The approach is a formal one, rooted in automata theory.
The following issues are addressed:
- Groundwork: Automata, Labelled Transitions systems, specification of processes.
- How to identify and distinguish processes by observation?
- What is conformance in our framework?
- how to derive test cases from a transition system?
- How far can we get with the derived test-cases?
- how to incorporated the quantitative notion of time into test cases?
A more accurate overview over the structure of the lecture will be available at the end of the semester. :-)
Exam
At the end of the semester will be a written exam for Master students. Prerequisite for this exam is a sufficiently high number of points in the home work assignments. The homework can be worked on in groups of 3.
Diploma students can combine this course most conveniently with Model Checking, AMC, and other courses of Prof. Katoen or Dr. Noll.
Material
There will be a script, provided in parts as PDF on this web page. This will be a similar, but extended version of the script from last year.
There will be no slides. The major part of the lecture is developed on the blackboard.
Additional Reading Material
In particular with respect to the ioco theory, the following reference might prove useful.
- Jan Tretmans. Testing Techniques. University of Twente, Radboud University Nijmegen, 2002/2004. Course notes of J. Tretmans, who developed the ioco theory. Thanks for sharing.
- Jan Tretmans. Model Based Testing with Labelled Transition Systems
In Hierons, R.M. and Bowen, J.P. and Harman, M. Formal Methods and Testing, LNCS 4949, Springer-Verlag, 2008. A tutorial-style introduction into ioco. Only freely accessible with an RWTH IP-Number.
Extra Material
Extra material will be provided as the course progresses. Below are two references from last year. Brush up your knowledge on Automata Theory (especially everything related to regular languages). It will come in handy.
- A method to eliminate tau-transitions (= epsilon transitions) from LTS (= finite automata) Note that finite LTS are basically finite automata where every state can be seen as accepting state. The trace set is thus the language of the LTS. The method comes from "Lawson: Finite Automata. Chapman & Hall, 2004". Note that the pdf file is only accessible from within the rwth-aachen.de domain.
- The powerset construction mentioned in the exercise class of May 22 is described in "J.E. Hopcroft, R. Motwani, J.D. Ullmann: Introduction to Automata Theory, Languages, and Computation, 2nd ed., Addison-Wesley, 2001". Also minimization of deterministic finite automata is explained, which also applicable to minimize LTS.
Errata
Mistakes in the script go here.
Language
The lecture will be given in english.
Literature
In General
Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and
Alexander Pretschner, editors, Model-Based Testing of Reactive Systems
(Advanced Lectures), Volume 3472 of Lecture Notes in Computer
Science. Springer-Verlag, 2005.
Alexander Pretschner, editors, Model-Based Testing of Reactive Systems
(Advanced Lectures), Volume 3472 of Lecture Notes in Computer
Science. Springer-Verlag, 2005.
First Part
Chapter 5 of the Broy... book.
Second Part
coming soon
Third part
Prerequisites
Automata Theory (e.g. ATFS)
