Seminar Model-Based Testing

Sommersemester 2006
Betreuer: Katoen, Bohnenkamp, Noll
Plätze: 15
Art der Veranstaltung: Wöchentlicher Vortrag
Termin: tba

Introduction

Testing is one of the most natural approaches to find out about the behaviour of software. It is the primary tool to find bugs, and it is used by everybody who writes programs. However, manual, ad-hoc testing is time-consuming, error-prone, and most of all, boring. Automatisation of testing is thus most desirable in order to decrease the number of bugs in software as much as possible.

The cans and cannots of testing have been a topic of theoretical computer science since the earliest days. The observation that a computer and its program is in principle nothing more than a finite automaton made the jump to an entirely mathematical (i.e. automata-theoretical) treatment of testing quite easy. Already in 1956, Edward Moore set a framework for the research on testing that was to come.

50 years later, testing is (again) a busy research area. Formal model-based testing (FMBT) is a most promising approach to systematic testing of software systems. The system under test is described as a formal model, as, for example, automata or labelled transition systems, and FMBT theories describe notions of correctness of an implmentation w.r.t. a model. Most importantly, these theories describe algorithms to derive and execute test-cases from the model, which are proven to be correct w.r.t to the correctness relation, and, under circumstances, even complete.

FMBT approaches targeted at functional correctness are known for quite some years now, and the theory has already found its way in tools like TorX and TGV. The aim of this seminar is to provide an overview over the main results and techniques on formal model-based testing in the spirit of Moore and his successors.

Prerequisites

Vordiplom or Bachelor in Computer Science.

It is possible to write the manuscript and to give the presentation in both German or English.

Registration

Registration to this seminar is handled via the central registration service of the CS Department. Registration deadline is January 27th, 2006.

First meeting

We will meet first on Friday, Feb. 10 2006, at 13:00 in the Seminar room of Informatik 3 (Room 4312).

Time and Place

We will meet weekly on Thursdays, from 8:15 to 10:00. Since there are 18 participants, there will be a couple of weeks in the semester with an extra meeting, or two presentations in a row. Time and place of these we will be negotiated in the introductory session, beginning of February. We will meet in the seminar room of Informatik 2 (Room 4201b), or, if that proves to be too cramped, in room 6019.

Organization

Every participant works on one subject.
Written report, $\approx$ 15-20 pages.
45 min presentation
German or English
2 presentations weekly
Seminar takes place Thursdays from 8:15 to 10:00.
First Session: April 27, 2006.

Deliverables

immediately: get literature from web or from library, learn all that seems to be important about the subject. Contact advisor if there are problems.
6 weeks prior to talk (or earlier): contact advisor and discuss your ideas about the presentation and report
2 weeks prior to talk: final version of report
1 week prior to talk: discuss presentation (have slides prepared)

Topics

The seminar is mostly based on chapters from the following book:

Model-Based Testing of Reactive Systems--- Advanced Lectures. Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner (Eds.). Vol 3472 of Lecture Notes in Computer Science. Springer-Verlag, 2005.

Nr	Topic	Literature	advisor
1	Homing and Synchronsising Sequences	[23]	CK
2	State Identification	[19]	SR
3	State Verification	[8]	TN
4	Conformance Testing	[16,20,21,25]	TN
5	Preorders	[12]	JPK
6	Preorder-related testing	[27]	HB
7	IO-automata-based testing	[26,18,28]	HB
8	Probabilistic Testing	[29]	JPK
9	Timed Testing: Theory	[9]	HB
10	Timed Testing: TA-approaches	[10]	HB
11	Symbolic Testing	[15]	HB
12	Run-Time Verification	[1,24]	TN
13	Black-Box Checking	[22]	TN
14	On the relation of Testing and Model-Checking	[14,2,7]	MN
15	Coverage and test-selection	[17]	HB
16	Testing at Microsoft	[3]	HB
17	Testing and the UML	[13]	HB
18	Testing Tools: TorX and TGV	[4,5,6]	HB

Who is doing what and when

Nr	Topic	advisor	student	Presentation
1	Homing and Synchronsising Sequences	CK	Rabinovich, Roman	27. April 2006
2	State Identification	SR	Tummel, Christian	27. April 2006
3	State Verification	TN	Koemm, Nikolaus	4. Mai 2006
4	Conformance Testing	TN	Kosse, Tim	4. Mai 2006
5	Preorders	JPK	Zimmermann, Ruben	11. Mai 2006
6	Preorder-related testing	HB	Färber, Ines	11. Mai 2006
7	IO-automata-based testing	HB	Wittenhagen, Moritz	18. Mai 2006
8	Probabilistic Testing	JPK	Jonas, Markus	18. Mai 2006
9	Timed Testing: Theory	HB	Horbert, Esther F.	verschoben auf 6. Juli 2006
10	Timed Testing: TA-approaches	HB	Vossemer, Tobias	1. Juni 2006
11	Symbolic Testing	HB	Klumb, Florian	22. Juni 2006
12	Run-Time Verification	TN	Tamkus, Birgit	22. Juni 2006
13	Black-Box Checking	TN	Namozova, Takhmina	29. Juni 2006
14	On the relation of Testing and Model-Checking	MN	Uysal, Merih Seran	29. Juni 2006
15	Coverage and test-selection	HB	Jansen, Thomas	6. Juli 2006
16	Testing at Microsoft	HB	Kamin, Volker
9	Timed Testing: Theory	HB	Horbert, Esther F.
17	Testing and the UML	HB	Watermeyer, Daniel	13. Juli 2006
18	Testing Tools: TorX and TGV	HB	Moers, Matthias	13. Juli 2006

Advisors

JPK: Joost-Pieter Katoen, katoen@cs.rwth-aachen.de, E1, Raum 4214
HB: Henrik Bohnenkamp, henrik@cs.rwth-aachen.de, E1, Raum 4210
SR: Stefan Rieger, rieger@cs.rwth-aachen.de, E1, Raum 4206
CK: Carsten Kern, kern@cs.rwth-aachen.de, E1, Raum 4206
TN: Thomas Noll, noll@cs.rwth-aachen.de, E1, Raum 4211
MN: Martin Neuhäußer, marneu@cs.rwth-aachen.de, E1, Raum 4207

Literature

1: Url of the Eagle tool.
http://yangtze.cs.uiuc.edu/~ksen/eagle/.
2: Homepage of John Rushby.
http://www.csl.sri.com/users/rushby/abstracts/sefm04.
3: Microsoft Research Webpage.
http://research.microsoft.com/projects/specexplorer/.
4: Url of the TorX project.
http://fmt.cs.utwente.nl/tools/torx/introduction.html.
5: Url of the TGV project.
http://www.irisa.fr/vertecs/Logiciels/TGV.html.
6: Url of the CADP.
http://www.inrialpes.fr/vasy/cadp/.
7: Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar.
Generating tests from counterexamples.
In Proceedings of the 26th International Conference on Software Engineering (ICSE 2004, Edinburgh, May 26-28), pages 326-335. IEEE Computer Society Press, Los Alamitos (CA), 2004.
8: Henrik Björklund.
State Verification, chapter 3.
Volume 3472 of Broy et al. [11], 2005.
9: Laura Brandán Briones and Ed Brinksma.
A test generation framework for quiescent real-time systems.
In Jens Grabowski and Brian Nielsen, editors, Formal Approaches to Testing of Software (FATES), number Technical Report SEA-SR-01. Kepler University Linz, 2004.
Pre-print.
10: Laura Brandán Briones and Matthias Röhl.
Test-Derivation from Timed Automata, chapter 8.
Volume 3472 of Broy et al. [11], 2005.
11: Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner, editors.
Model-Based Testing of Reactive Systems: Advanced Lectures, volume 3472 of LNCS.
Springer-Verlag, 2005.
12: Stefan D. Bruda.
Preorder Relations, chapter 5.
Volume 3472 of Broy et al. [11], 2005.
13: Zhen Ru Dai.
The UML 2.0 Testing Profile, chapter 17.
Volume 3472 of Broy et al. [11], 2005.
14: Dejan Desovski.
Combining testing and model-checking for verifcation of high-assurance systems.
In HASE '04 (Proceedings). IEEE, 2004.
15: L. Frantzen, J. Tretmans, and T.A.C. Willemse.
Test generation based on symbolic specifications.
In J. Grabowski and B. Nielsen, editors, FATES 2004, number 3395 in LNCS, pages 1-15. Springer-Verlag, 2005.
16: Angelo Gargantini.
Conformance Testing, chapter 4.
Volume 3472 of Broy et al. [11], 2005.
17: Chrostophe Gaston and Dirk Seifert.
Evaluatinig Coverage-Based Testing, chapter 11.
Volume 3472 of Broy et al. [11], 2005.
18: Lex Heerink.
Ins and Outs in Refusal Testing.
PhD thesis, University of Twente, 1998.
19: Moez Krichen.
State Identification, chapter 2.
Volume 3472 of Broy et al. [11], 2005.
20: David Lee and Mihalis Yanakakis.
Principle and methods of testing finite state machines.
Proc. of the IEEE, 84(8):1090-1123, 1996.
Invited Paper.
21: E. F. Moore.
Gedanken-experiments on sequential machines.
In Automata Studies, number 34 in Annals of Math. Studies, pages 129-153. Princeton Univ. Press, Princeton, NJ, 1956.
22: Doron Peled, Moshe Y. Vardi, and Mihalis Yannakakis.
Black box checking.
Journal of Automata, Languages and Combinatorics, 7(2):225-246, 2002.
23: Sven Sandberg.
Homing and Synchronizing Sequences, chapter 1.
Volume 3472 of Broy et al. [11], 2005.
24: Leonardo Mariani Severine Colin.
Run-Time Verification, chapter 18.
Volume 3472 of Broy et al. [11], 2005.
25: Katsuhiko Takahashi, Akio Fujiyoshi, and Takumi Kasai.
A polynomial time algorithm to infer sequential machines.
Systems and Computers in Japan, 34(1):59-67.
26: J. Tretmans.
Test generation with inputs, outputs, and repetitive quiescence.
Software - Concepts and Tools, 17:103-120, 1996.
27: Valéry Tschaen.
Test Generation Algorithms based on Preorder Relations, chapter 6.
Volume 3472 of Broy et al. [11], 2005.
28: Machiel van der Bijl and Fabien Pereux.
I/O-automata Based Testing, chapter 7.
Volume 3472 of Broy et al. [11], 2005.
29: Verena Wolf.
Testing for Probabilistic Testing, chapter 9.
Volume 3472 of Broy et al. [11], 2005.

Webmaster

Disclaimer

Last modified: 2006-06-22 09:02 UTC