Invited Speakers

Patrice Godefroid

Software Reliability Research
Microsoft Research

Darko Marinov

Department of Computer Science
University of Illinois at Urbana-Champaign





09:00 - 10:30 SESSION 1

Opening and Welcome
Bernd Finkbeiner, Yuri Gurevich, Alexander K. Petrenko

Invited Talk: Whitebox Fuzzing for Security Testing

Patrice Godefroid

10:30 - 11:00 Tea break

11:00 - 12:30 SESSION 2

Automated Software Testing of Asynchronous Systems

Percy Pari Salas and Paddy Krishnan

Model-based Kernel Testing for Concurrency Bugs through Counter Example Replay
Moonzoo Kim, Shin Hong, Changki Hong, and Taeho Kim

On the Use of Uniform Random Generation of Automata for Testing
Frédéric Dadeau, Pierre-Cyrille Heam, and Jocelyn Levrey

12:30 - 14:00 Lunch

14:00 - 15:30 SESSION 3

Invited Talk: Model-Based Testing Using Test Abstractions
         Darko Marinov

Test Case Generation by Contract Mutation in Spec#
Willibald Krenn and Bernhard K. Aichernig

15:30 - 16:00 Tea break

16:00 - 18:00 SESSION 4

Conformance Testing of Hybrid Systems with Qualitative Reasoning Models
Harald Brandl, Bernhard K. Aichernig, and Franz Wotawa

Computing Optimal Distinguishing Tests for Non-deterministic Systems Using Linear Time DNNF Algorithms
Anika Schumann, Martin Sachenbacher, and Jinbo Huang

Model Based Testing of a Network on Chip Component
Leonidas Tsiopoulos and Manoranjan Satpathy

jSynoPSys -- A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines
Frédéric Dadeau and Régis Tissot

18:00 - 18:30 Discussion and Closing




Aims and Scope

The workshop is devoted to model-based testing of both software and hardware.  Model-based testing is closely related to model-based specification.  Models are used to describe the behavior of the system under consideration and to guide such efforts as test selection and test results evaluation.  Both testing and verification are used to validate models against the requirements and check that the implementation conforms to the specification model.

Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model.

Techniques to support model-based testing are drawn from diverse areas, like formal verification, model checking, control and data flow analysis, grammar analysis, and Markov decision processes.

The intent of this workshop is to bring together researchers and users of models for to discuss the state of the art in theory, applications, tools, and industrialization of model-based specification, testing and verification.

Workshop History

MBT 2009 is the fifth event in a series of ETAPS satellite workshops. MBT 2004, historically the first meeting to focus on model-based testing, was held March 27-28, 2004, in Barcelona, Spain. MBT 2006 was held March 25-26, 2006, in Vienna, Austria, MBT 2007 on March 31 - April 1, 2007, in Braga, Portugal, and MBT 2008 on March 30, 2008, in Budapest, Hungary. The proceedings have appeared in ENTCS (volumes 111, 164, 190, 220).

Submission Topics

Original submissions are solicited from industry and academia. They are invited to present their work, plans, and views related to model-based testing. The topics of interest include but are not limited to:

Online and offline test sequence generation methods and tools
Test data selection methods and tools
Runtime verification
Model-based test coverage metrics
Automatic domain/partition analysis
Combination of verification and testing
Models as test oracles
Scenario based test generation
Meta programming support for testing
Formalisms suitable for model-based testing
Application of model checking techniques in model-based testing
Game-theoretic approaches to testing
Model-based testing in industry: problems and achievements

Important Dates

Paper submissions – December 22, 2008 (extended)
Notification of acceptance – January 20, 2009
Final versions – February 5, 2009
Workshop – March 22, 2009

Paper Submission

Online paper submission has closed.

RESEARCH PAPERS should be limited to 15 pages in ENTCS format (, prentcsmacro.sty), describing significant research results based on sound theory or experimental assessment.

We also solicit INDUSTRY EXPERIENCE PAPERS, about the use of model-based testing in industrial environments. Such papers should be limited to 15 pages too.

Workshop proceedings will be distributed by the organizers of ETAPS’09. It is intended also that selected contributions will be published in a journal.

Organizing Committee

Bernd Finkbeiner (Universität des Saarlandes, Germany)
Yuri Gurevich (Microsoft Research, USA)
Alexander K. Petrenko (Institute for System Programming of Russian Academy of Sciences)

Program Committee

Bernhard K. Aichernig (Graz University of Technology, Austria)
Jonathan Bowen (Museophile Limited, UK)
Mirko Conrad (The MathWorks GmbH, Germany)
John Derrick (University of Kent, UK)
Bernd Finkbeiner (Universität des Saarlandes, Germany)
Marie-Claude Gaudel (Universite Paris-Sud, France)
Susanne Graf (Verimag, Grenoble, France)
Yuri Gurevich (Microsoft Research, USA)
Ziyad Hanna (Jasper Design Automation, USA)
Antti Huima (Conformiq Software Ltd., Finland)
Alexander S. Kossatchev (ISP RAS, Russia)
Darko Marinov (University of Illinois, USA)
Bruno Marre (Universite Paris-Sud, France)
Alexander K. Petrenko (ISP RAS, Russia)
Alexandre Petrenko (Computer Research Institute of Montreal, Canada)
Natasha Sharygina (University of Lugano, Switzerland)
Nikolai Tillmann (Microsoft Research, USA)
Jan Tretmans (Embedded Systems Institute, Eindhoven, The Netherlands)
Nina Yevtushenko (Tomsk State University, Russia)