Title
Model-Based Testing
Type
Weekly Seminar (Hauptstudium) in Theoretical CS for Bachelor, Master and Diplom students.
News
- Here are the slides of the kick-off meeting.
Time Schedule
The meetings will take place weekly on tuesday at 4 p.m. in room 4201b.
When | Date | What | Who | |
|---|---|---|---|---|
KW 17 | 27.4. | Ansgar Prüne | ||
KW 18 | 4.5. | Marcel Bosling | ||
KW 19 | 11.5. | IO-automata-based Testing (slides) | ||
KW 20 | 18.5. | Fabian Kürten | ||
KW 22 | 1.6.. | Christian Röller | ||
KW 23 | 8.6. | Malte Kampschulte | ||
KW 24 | 15.6. | Bernhard Ern | ||
KW 25 | 22.6. | Conformance Testing of Components | Patrick Wallukat | |
KW 26 | 29.6. | Stefan Gottschalk | ||
KW 27 | 6.7. | Black-Box Checking | Alexander Braining | |
KW 28 | 13.7. | On the relation of Testing and Model-Checking | Mareike Bültmann | |
KW 29 | 20.7. | Testing with Model Checkers | Katrin Hölldobler |
Contents
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 UPPAAL Tron. 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.
Topics
Nr. | Topic | Student | Supervisor | |||
|---|---|---|---|---|---|---|
1 | Homing and Synchronising Sequences | Ansgar Prüne | ||||
2 | Preoders | Marcel Bosling | ||||
3 | IO-automata-based Testing | |||||
4 | Timed Testing | Christian Röller | ||||
5 | Testing-Tool: UPPAAL Tron | |||||
6 | Testing of Hybrid Systems | Malte Kampschulte | ||||
7 | Symbolic Testing | Bernhard Ern | ||||
8 | Conformance Testing of Components | |||||
9 | Customized Probabilistic Testing | |||||
10 | Testing Scenario for Probabilistic Testing | |||||
11 | Black-Box Checking | Alexander Braining | ||||
12 | On the relation of Testing and Model-Checking | Mareike Bültmann | ||||
13 | Testing with Model Checkers | Katrin Hölldobler | ||||
14 | Coverage and test-selection | Fabian Kürten | ||||
15 | Testing at Microsoft | Stefan Gottschalk |
People involved
- Henrik Bohnenkamp (Contact person for questions, henrik at cs dot rwth-aachen dot de)
- Sabrina von Styp
- Joost-Pieter Katoen
First Meeting
The first meeting will take place in February (last week of the semster), in the seminar room of I2, Room 4201b, Building E1. All participants should have received a link to a doodle poll to find a good day and time for the meeting (at 29 Jan 2010).
Attending this meeting is mandatory.
Literature
Some papers can be found in
- 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. Accessible for free from the RWTH networks (as all other LNCS volumes).
Topic(s) | Literature | |
|---|---|---|
1 | Sven Sandberg. Homing and Synchronizing Sequences. chapter 1. Volume 3472 of Broy et al.2005. | |
2 | Stefan D. Bruda. Preorder Relations. chapter 5. Volume 3472 of Broy et al. 2005. | |
3 | Lex Heerink. Ins and Outs in Refusal Testing. PhD thesis, University of Twente, 1998 | |
3 | Jan Tretmans. Test generation with inputs, outputs, and repetitive quiescence. Software - Concepts and Tools, 17:103-120, 1996. | |
3 | Machiel van der Bijl and Fabien Pereux. I/O-automata Based Testing, chapter 7.Volume 3472 of Broy et al. 2005. | |
4 | Moez Krichen and Stavros Tripakis. Black-Box Conformance Testing for Real-Time Systems. Volume 2989 of LNCS, pp. 109-126, Springer 2004 | |
4 | Julien Schmaltz and Jan Tretmans. On Conformance Testing for Timed Systems. (FORMATS’08), F. Cassez and C. Jard (eds), pp. 249-263, LNCS 5215, Springer, 2008 | |
4 | Brandán Briones, L. and Brinksma, H. (2004) A test generation framework for quiescent real-time systems - extended version. Technical Report TR-CTIT-04-40, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625 [ .pdf ] | |
5 | Andreas Hessel, Kim G. Larsen, Marius Mikucionis, Brian Nielsen, Paul Pettersson and Arne Skou. Testing Real-Time Systems Using UPPAAL. Formal Methods and Testing. Springer Berlin / Heidelberg., 2008. | |
5 | Homepage of UPPAAL Tron www.cs.aau.dk/~marius/tron/ | |
6 | M. van Osch. Model-based Testing of Hybrid Systems. In J. Tretmans, editors, Tangram: Model-based integration and testing of complex high-tech systems - A collaborative Research Project on Multidisiplinary Integration and Testing of Embedded Systems, Chapter 9, 2007 | |
7 | L. Frantzen, J. Tretmans, and T.A.C. Willemse. Test Generation Based on Symbolic Specifications. In J. Grabowski and B. Nielsen, editors, Formal Approaches to Software Testing - FATES 2004, number 3395 in LNCS, pp. 1-15. Springer, 2005. [ .pdf ] | |
7 | L. Frantzen, J. Tretmans, and T.A.C. Willemse. A Symbolic Framework for Model-Based Testing. In K. Havelund, M. Núńez, G. Rosu, and B. Wolff, editors, Formal Approaches to Software Testing and Runtime Verification - FATES/RV 2006, number 4262 in LNCS, pp. 40-54. Springer, 2006. [ .pdf ] | |
8 | L. Frantzen and J. Tretmans. Model-Based Testing of Environmental Conformance of Components. In F.S. de Boer and M. Bonsangue, editors, Formal Methods of Components and Objects - FMCO 2006, number 4709 in LNCS, pp. 1-25. Springer, 2007. [ .pdf ] | |
9 | Luis F. Llana-Díaz, Manuel Núńez and Ismael Rodríguez. Customized Testing for Probabilistic Systems. pp. 87-102, LNCS Volume 3964, Spinger, 2006. | |
9 | Natalia López, Manuel Núńez and Ismael Rodríguez. Formal Specification of Symbolic-Probabilistic Systems. pp. 114-127, in LNCS Volume 3236, Spinger, 2004. | |
9, 10 | Verena Wolf. Testing for Probabilistic Testing, chapter 9. Volume 3472 of Broy et al., 2005. | |
10 | L. Cheung and M.I.A. Stoelinga and F.W. Vaandrager. A Testing Scenario for Probabilistic Processes . Journal of the ACM 2007. [ pdf ] | |
11 | Doron Peled, Moshe Y. Vardi, and Mihalis Yannakakis. Black box checking. Journal of Automata, Languages and Combinatorics, 7(2):225-246, 2002. | |
12 | Dejan Desovski. Combining testing and model-checking for verifcation of high-assurance systems. In HASE '04 (Proceedings). IEEE, 2004. | |
12 | Homepage of John Rushby. www.csl.sri.com/users/rushby/abstracts/sefm04. | |
12 | Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Generating tests from counterexamples. In Proceedings of ICSE 2004, Edinburgh, pp. 326-335. IEEE Computer Society Press, Los Alamitos (CA), 2004. | |
13 | Gordon Fraser, Franz Wotawa, Paul E. Ammann. Testing with Model Checkers: A Survey. Journal for Software Testing, Verification and Reliability 2009, pp. 251-261 | |
14 | Chrostophe Gaston and Dirk Seifert. Evaluatinig Coverage-Based Testing, chapter 11. Volume 3472 of Broy et al., 2005. | |
15 | Microsoft Research Webpage. http://research.microsoft.com/projects/specexplorer/ |
