Call for Participation
GI/Dagstuhl Research Seminar
January 12-15, 2004, Schloss
Theme of the seminar
Testing is the primary hardware and software validation 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. But a
comprehensive account of the area of formal testing is missing. The
goal of this seminar is to elaborate a volume providing an in-depth
exposure of this emerging area, especially to make it easily
accessible to new researchers in this field.
Aim of the seminar
The aim of the seminar is to bring together (primarily young) researchers
working in or starting to work in this area (PhD students, postdocs, fresh
maybe even MSc students; also established researchers might apply). The
seminar will be
devoted to the assembly of a structured overview (in terms of presentations
and papers) of the state-of-the-art.
The organisers will select the participants on the basis of their
application (see below). Selected participants will be approached by
the coordinators and will be assigned a theme, thereby taking into
account the preferences of the applicants as much as possible. The
participants will then write an overview paper (up to 30--40 pages) on
the assigned theme, supervised by the coordinator; the papers listed
below form a starting point for doing so. During the seminar in
January 2004 in Dagstuhl, the overview paper has to be presented
(45 minutes) and discussed. Some of the themes listed below are so
large that working on them in a 2-person group is possible.
The seminar papers written will be collected and published with a
German publisher. In fact, based on the quality of the final papers, a
publication as a tutorial volume in the LNCS series of Springer-Verlag
is very likely. In order to ease the publication process, we strongly
encourage the papers to be written using LaTeX using Springer's lncs
In total, we envisage that taking part in the seminar, including the
reading, writing, presenting and travelling, will "cost" at least 5 to 6
weeks of work (full time). Note, however, that esp. for PhD students, this
type of work has to be done anyway, as part of their PhD studies.
The seminar is organised by
- Manfred Broy, Technical University of Munich, Germany
- Bengt Jonsson Uppsala University, Sweden
Katoen, University of Twente, Netherlands
- Martin Leucker, Uppsala University, Sweden, (Coordinator)
- Alexander Pretschner, Technical University of Munich, Germany
Time and location
The seminar is organised as a GI/Dagstuhl-seminar from January 12, 2004
(Monday, arrival) through January 15, 2004 (Thursday) in the International Conference and Research Center
for Computer Science at Schloss Dagstuhl. Dagstuhl lies about halfway
between Saarbrücken and Trier and is ideally suited for a research
seminar because of its excellent library and special atmosphere.
Registration fee for all participants will be 100 Euro; this includes
accommodation, all meals and coffee/tea breaks. This extremely low fee is
made possible through the sponsorship of the Gesellschaft für
Participants are selected on the basis of a good scientific qualification.
Participants can apply by sending a short curriculum vitae (with list of
publications) and a letter of reference from a professor (in case of MSc
or PhD students). Also indicate the topics of your interest!
Applications (including a list of preferred topics) should be sent
electronically (as PS or PDF) by August 30, 2003 to Martin Leucker.
- July 01: launch of call for participation
- August 30: deadline for applications
- September 30: notification on participation (changed)
- November 2003: first version of seminar paper
- December 2003: revised versions of seminar paper
- January 12-15, 2004: Dagstuhl seminar
- March 2004: final camera-ready seminar papers due
- Spring 2004: publication of seminar volume
We will give an detailed account to formal approaches of testing as
well as relations to other validation techniques like model checking.
There are several schools of formal testing. We will give an
account to some of them providing the basis for a comparison. We will
show the similarities and differences in each approach. In general, we
concentrate on so-called black-box testing. In this setting,
the system under test is not given explicitly but may only be
analysed using interaction in terms of input and output actions.
For each of the theme areas, we list literature below. Most of these
papers can be found via the citeseer or the dplb web site. The coordinators can
also help in locating the literature. By no means is the following
catalog of literature meant to be comprehensive, and authors are
expected to provide further material.
Coordinator: Martin Leucker and Bengt Jonsson
During the last 50 years, a rich testing theory has been developed for
testing finite state machines that produce outputs on state
transitions after receiving inputs (also known as Mealy
machines). Typical problems addressed in the domain of finite state
machine testing are
- Homing Sequence: Determine the final state after the test
- State Identification: Identify the unknown initial state
- State Verification: Verify that a machine is in a
- Machine Verification/Fault Detection/Conformance Testing: Check
whether two given machines are equivalent
- Machine Identification: Identify an unknown machine
Further keywords in this area are transition tour, postman,
unique input/output sequence etc.
An overview of testing finite state machines is given in
[LY96]. It will serve as a starting point for the chapters
dealing with testing finite state machines.
Coordinator: Joost-Pieter Katoen
The theory of testing transition systems was initiated by the
work of De Nicola and Hennessy in [MN83]. The basic goal
is to test whether one transition system is an implementation
of another one. Therefore, several notions of implementation
relations were introduced and studied. A usually infinite number of
test cases is identified that characterizes the implementation
relation. The work was later extended towards transition systems in
which input and output actions are distinguished.
In [BT01], an annotated bibliography for this
approach is given which points out the relevant work in this area.
Recently, extensions to cover real-time or probabilistic systems have
been studied, for example in [SVD01] and
To turn this approach into a practical method, a finite number of test
cases has to be selected out the infinite set describing the
implementation relation. The goal is to choose test cases that cover
the infinite set, as good as possible. This approach is studied in
This model also assumes that the tester communicates with the system
under test is a synchronous manner. In practice, however, the two
systems often interact via queues. [TV92] discusses this
Coordinator: Alexander Pretschner
In the setting of model-based testing, a formal model of an
implementation is given. The goal is to check whether the
implementation conforms to the model. Usually, testing is restricted
to certain interesting test cases for which conformance is
checked. Here, a test case is a sequence of input and (expected)
output values. Test cases are usually determined in terms of
test specifications that specify which part of the system is to
be tested. Often, test specifications are given in form of
Typical models are extended finite state machines in which
states are enriched with data or time variables. Thus, the model is
usually not concrete in the sense that every state of the
system is represented as a single state in the model. It is
abstract so that symbolic test cases require
instantiation to concrete ones. Overviews are given in
[DBG01,FHP02, P02]. Other input languages that
have been used for test case generation include statecharts,
CSP, Lotos, SDL, extended FSMs, etc. Real-time testing will also
be an issue [P02, N00].
There is a huge number on papers on specifying and generating test
cases, for example [FHNS02]. A selection of these methods
describing basic ideas will be presented. The focus is on techniques
rather than on which test cases to specify. One approach, for example,
is to specify coverage criteria by means of temporal logic. Test
cases are then witnesses or counter examples for the underlying
formula and the model. This is studied in
[RH01,EFM97,HLSU02,Pre03]. Among model checkers, test
case generation technology includes symbolic execution or
deductive theorem proving.
Apart from test case derivation, it is important to check that the
output obtained by executing the test case is as expected. Techniques
like test oracle generation are important for that
Coordinator: Alexander Pretschner
Clearly not restricted to these, the following tools will be discussed:
- AUTOLINK A tool developed by Telelogic and that is applied
quite often in industry [KGH+98]
- TORX is a tool developed within the Dutch Côte de
- TGV [FJJV96,JM99] and TVEDA [CGPT96],
both developed at INRIA. The ideas of both tools have been combined
into TESTCOMPOSER, which is part of the commercial SDL tool
set OBJECTGEODE [KJG99]
- AUTOFOCUS is a CASE tool developed at the Technical
University Munich and offers model-based testing facilities
[HSE97, SPHP02, PPS+03]
- Lurette [RWN+98], Lutess [BOP+00], and Gatel [MA00] are tools for test case generation
Some of the tools have been compared in [Gog01].
Case studies showing the benefit of formal testing in practice will be
given, e.g. [PPS+03].
Coordinator: Martin Leucker
To allow different testing tools to be employed in practice, standards
have to be developed for test execution, i.e., the interaction of a
testing tool with the system under test. TTCN-3 [Wil01]
is a language for describing the test setup as well as test cases. A
compiler then produces a program that runs the given tests cases.
Coordinator: Joost-Pieter Katoen
To apply testing in practice, a uniform testing methodology is
helpful. ISO 9646 [CFP96] defines how to proceed when
testing a system. Other ideas are presented in
Coordinator: Bengt Jonsson
Usually, one assumes that the system under test behaves
deterministically. In practice, this assumption is sometimes not
adequate. Testing of non-deterministic systems is studied for example
Coordinator: Martin Leucker
Model checking is one of the key techniques in verifying hard-
but also software systems. The formal theory of model checking is well
developed in contrast to the domain of testing. It is, however, likely
that many achievements in the domain of model checking are valuable
for formal testing as well. Recently, several attempts have been made.
Adaptive model checking [GPY02] combines
learning [Ang87] of automata and model checking
to study an underlying system.
In the domain of run-time verification, one studies the
question how to check properties of a system while executing it. In
[HR02], for example, monitors for temporal logic
formulas are generated that check whether a property is satisfied or
violated. Obviously, there is a strong relationship between
model-checking, run-time verification, and testing which will be
elaborated in this part.
Learning regular sets from queries and counterexamples.
Information and Computation, 75:87-106, 1987.
H. Buwalda and M. Kasdorp.
Getting Automated Testing Under Control.
Software Testing& Quality Engineering, pages 39-44,
L. duBousquet, F. Ouabdesselam, L. Parissis, J.-L. Richier,
and N. Zuanon.
Specification-Based Testing of Synchronous Software
In Proc. 5th Intl. Workshop on Formal Methods for Industrial
Critical Systems, 2000.
G. Bochmann and A. Petrenko.
Protocol testing: review of methods and relevance for software
In /Proc. Intl. Symp. on Software testing and analysis, pages
/pages 109-124, 1994.
On the coverage of partial validations.
In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo,
editors, Algebraic Methodology and Software Technology (AMAST '93),
Proceedings of the Third International Conference on Methodology and Software
Technology, Workshops in Computing, pages 245-252. Springer, 1994.
Ed Brinksma and Jan Tretmans.
Testing transition systems: An annotated bibliography.
Lecture Notes in Computer Science, 2067:187-??, 2001.
Ana R. Cavalli, Jean Philippe Favreau, and Marc Phalippou.
Standardization of formal methods in conformance testing of
Computer Networks and ISDN Systems, 29(1):3-14, December 1996.
M. Clatin, R. Groz, M. Phalippou, and R. Thummel.
Two approaches linking test generation with verification techniques.
In A. Cavalli and S. Budkowski, editors, 8th International
Workshop on Protocol Test Systems. Chapman & Hall, 1996.
J. Dushina, M. Benjamin, and D. Geist.
Semi-Formal Test Generation with Genevieve.
In Proc. DAC, 2001.
Laura K. Dillon and Y. S. Ramakrishna.
Generating oracles from your favorite temporal logic specifications.
In Foundations of Software Engineering, pages 106-117, 1996.
A. Engels, L. Feijs, and S. Mauw.
Test generation for intelligent networks using model checking.
In Proc. TACAS '97, Int. Conf. on Tools and
Algorithms for the Construction and Analysis of Systems, volume 1217 of Lecture Notes in Computer Science, Enschede, The Netherlands, 1997. Springer
Loe M. G. Feijs, Nicolae Goga, Sjouke Mauw, and Jan Tretmans.
Test selection, trace distance, and heuristics.
In Ina Schieferdecker, Harmut könig, and Adam Wolisz, editors,
Proceedings of the IFIP 14th International Conference on Testing
Communicating Systems - TestCom 2002, volume 210 of IFIP Conference
Proceedings. Kluwer, 2002.
Galit Friedman, Alan Hartman, Kenneth Nagin, and Tomer Shiran.
Projected state machine coverage for software testing.
In Phyllis G. Frankl, editor, Proceedings of the ACM SIGSOFT
2002 International Symposium on Software Testing and Analysis (ISSTA-02),
volume 27, 4 of SOFTWARE ENGINEERING NOTES, pages 134-143, New York,
July 22-24 2002. ACM Press.
E. Farchi, A. Hartman, and S. Pinter.
Using a model-based test generator to test for standard
IBM Systems Journal, 41(1):89-110, 2002.
J. C. Fernandez, C. Jard, T. Jéron, and G. Viho.
Using on-the-fly verification techniques for the generation of test
In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings
of the Eighth International Conference on Computer Aided Verification CAV,
volume 1102 of Lecture Notes in Computer Science, pages 348-359, New
Brunswick, NJ, USA, July/August 1996. Springer Verlag.
Comparing TorX, autolink, TGV and UIO test algorithms.
Lecture Notes in Computer Science, 2078:379-??, 2001.
Alex Groce, Doron Peled, and Mihalis Yannakakis.
Adaptive model checking.
In Tools and Algorithms for the Construction and Analysis of
Systems (TACAS'02), volume 2280 of Lecture Notes in Computer Science,
pages 357-??, 2002.
Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, and Hasan Ural.
A temporal logic based theory of test coverage and generation.
In P. Stevens J.-P. Katoen, editor, Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'02), volume 2280 of Lecture
Notes in Computer Science, pages 327-241. Springer, 2002.
K. Havelund and G. Rosu.
Synthesizing monitors for safety properties.
In J.-P. Katoen and P. Stevens, editors, Proc. TACAS '02,
Int. Conf. on Tools and Algorithms for the Construction and
Analysis of Systems, volume 2280 of Lecture Notes in Computer Science,
pages 324-356. Springer Verlag, 2002.
F. Huber, B. Schätz, and G. Einert.
Consistent Graphical Specification of Distributed Systems.
In Proc. 4th Intl. Symp. of Formal Methods Europe (FME'97),
volume 1313 of Lecture Notes in Computer Science, pages 122 - 141.
Springer Verlag, 1997.
Specification and Test of Real-Time Systems
PhD Thesis, Aalborg University, Dept. of Computer Science, 2000.
T. Jéron and P. Morel.
Test generation derived from model-checking.
In N. Halbwachs and D. Peled, editors, Proceedings of the 11th
International Conference on Computer Aided Verification, Trento,
Italy, volume 1633 of Lecture Notes in Computer Science.
Springer-Verlag, July 1999.
B. Koch, J. Grabowski, D. Hogrefe, M. Schmitt
AutoLink---A tool for Automatics Test Generation From SDL Specifications
In Proc. IEEE Intl. Workshop on Industrial Strength Formal
Specification Techniques, October 1998.
A. Kerbra, T. Jéron, and R. Groz.
Automated test generation from SDL specifications.
In R. Dssouli, G. von Bochmann, and Y. Lahav, editors, SDL'99
The Next Millennium - Proceedings of the 9th SDL Forum, pages 135-152.
Elsevier Science, 1999.
D. Lee and M. Yannakakis.
Principles and methods of testing finite state machines - a survey.
Proc. IEEE, 84(8):1090-1126, 1996.
M.Hennessy and R. De Nicola.
Testing equivalences for processes.
In Proc. ICALP '83, 1983.
B. Marre and A. Arnould.
Test Sequence Generation from Lustre Descriptions: GATEL
In Proc. 15th IEEE Intl. Conf. on Automated Software Engineering, 2000.
J. Philipps, A. Pretschner, O. Slotosch, E. Aiglstorfer, S. Kriebel, and
Model-based test case generation for smart cards.
In In Proceedings of the 8th International Workshop on Formal
Methods for Industrial Critical Systems (FMICS 03), 2003.
Formal Methods for Test Automation -- Hard Real-Time Testing of
Controllers ofr the Airbus Aircraft Family
In Proc. Integrated Design and Process Technology, 2002.
Compositional generation for MC/DC test suites.
In Proceedings of TACoS'03, pages 1-11, 2003.
Electronic Notes in Theoretical Computer Science 82(6).
S. Rayadurgan and M. Heimdahl.
Coverage Based Test-Case Generation using Model Checkers.
In Proc. 8th Intl. Conf. and Workshop on the Engineering of
Computer Based Systems, pages 83-93, 2001.
P. Raymond, D. Weber, X. Nicollin and N. Halbwachs.
Automatic Testing of Reactive Systems.
In Proc. 19th IEEE Real-Time Symposium, 1998.
B. Schätz, A. Pretschner, F. Huber, and J. Philipps.
Model-based development of embedded systems.
In Advances in Object-Oriented Information Systems (OOIS'02),
volume 2426 of Lecture Notes in Computer Science, pages 298-311, 2002.
M.I.A. Stoelinga and F.W. Vaandrager.
A testing scenario for probabilistic automata.
In Proc. ICALP '2003, International Colloquium on
Automata, Lnaguages, and Programming, 2003.
Jan Springintveld, Frits Vaandrager, and Pedro R. D'Argenio.
Testing timed automata.
Theoretical Computer Science, 254(1-2):225-257, March 2001.
J. Tretmans and L. Verhaard.
A queue model relating synchronous and asynchronous communication.
In Proceedings of the International Conference on
Protocol Specification, Testing and Verification. North-Holland, 1992.
ETSI testing activities and the use of TTCN-3.
Lecture Notes in Computer Science, 2078:123-??, 2001.
Martin Leucker, July 01, 2003