Call for Participation

GI/Dagstuhl Research Seminar

Model-based Testing of Reactive Systems

January 12-15, 2004, Schloss Dagstuhl

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 PhDs, or 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.

Organisation

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 style.

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.

Organisers

The seminar is organised by

Manfred Broy, Technical University of Munich, Germany
Bengt Jonsson Uppsala University, Sweden
Joost-Pieter 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 Informatik.

Application

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.

Time table

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

List of theme areas and topics

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.

T1: Testing of finite state machines (3 chapters)

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 particular state
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.

T2: Preorder-based testing of labelled transition systems (4 chapters)

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 [SV03].

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 [FGMT02,Bri94].

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 problem.

T3: Further Model-based testing (3 chapters)

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 coverage criteria.

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 [DR96].

T4: Test generation tools and case studies (2 chapters)

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 Resyste project.
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 with Lustre

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].

T5: Test execution: TTCN-3 (1 chapter)

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.

T6: Test methods (1 chapter)

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 [BK99].

T7: Testing of non-deterministic systems (1 chapter)

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 in [BP94].

T8: Model checking and testing (3 chapters)

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.

Bibliography

[Ang87]: Dana Angluin.
Learning regular sets from queries and counterexamples.
Information and Computation, 75:87-106, 1987.
[BK99]: H. Buwalda and M. Kasdorp.
Getting Automated Testing Under Control.
Software Testing& Quality Engineering, pages 39-44, November/December 1999.
[BOP+00]: 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.
[BP94]: G. Bochmann and A. Petrenko.
Protocol testing: review of methods and relevance for software testing.
In /Proc. Intl. Symp. on Software testing and analysis, pages /pages 109-124, 1994.
[Bri94]: Ed Brinksma.
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.
[BT01]: Ed Brinksma and Jan Tretmans.
Testing transition systems: An annotated bibliography.
Lecture Notes in Computer Science, 2067:187-??, 2001.
[CFP96]: Ana R. Cavalli, Jean Philippe Favreau, and Marc Phalippou.
Standardization of formal methods in conformance testing of communication protocols.
Computer Networks and ISDN Systems, 29(1):3-14, December 1996.
[CGPT96]: 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.
[DBG01]: J. Dushina, M. Benjamin, and D. Geist.
Semi-Formal Test Generation with Genevieve.
In Proc. DAC, 2001.
[DR96]: Laura K. Dillon and Y. S. Ramakrishna.
Generating oracles from your favorite temporal logic specifications.
In Foundations of Software Engineering, pages 106-117, 1996.
[EFM97]: A. Engels, L. Feijs, and S. Mauw.
Test generation for intelligent networks using model checking.
In Proc. TACAS '97, $3^{th}$ 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 Verlag.
[FGMT02]: 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.
[FHNS02]: 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.
[FHP02]: E. Farchi, A. Hartman, and S. Pinter.
Using a model-based test generator to test for standard conformance.
IBM Systems Journal, 41(1):89-110, 2002.
[FJJV96]: J. C. Fernandez, C. Jard, T. Jéron, and G. Viho.
Using on-the-fly verification techniques for the generation of test suites.
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.
[Gog01]: N. Goga.
Comparing TorX, autolink, TGV and UIO test algorithms.
Lecture Notes in Computer Science, 2078:379-??, 2001.
[GPY02]: 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.
[HLSU02]: 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.
[HR02]: K. Havelund and G. Rosu.
Synthesizing monitors for safety properties.
In J.-P. Katoen and P. Stevens, editors, Proc. TACAS '02, $8^{th}$ 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.
[HSE97]: 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.
[N00]: B. Nielsen.
Specification and Test of Real-Time Systems
PhD Thesis, Aalborg University, Dept. of Computer Science, 2000.
[JM99]: 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.
[KGH+98]: 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.
[KJG99]: 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.
[LY96]: D. Lee and M. Yannakakis.
Principles and methods of testing finite state machines - a survey.
Proc. IEEE, 84(8):1090-1126, 1996.
[MN83]: M.Hennessy and R. De Nicola.
Testing equivalences for processes.
In Proc. ICALP '83, 1983.
[MA00]: B. Marre and A. Arnould.
Test Sequence Generation from Lustre Descriptions: GATEL
In Proc. 15th IEEE Intl. Conf. on Automated Software Engineering, 2000.
[PPS+03]: J. Philipps, A. Pretschner, O. Slotosch, E. Aiglstorfer, S. Kriebel, and K. Scholl.
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.
to appear.
[P02]: J. Peleska.
Formal Methods for Test Automation -- Hard Real-Time Testing of Controllers ofr the Airbus Aircraft Family
In Proc. Integrated Design and Process Technology, 2002.
[Pre03]: A. Pretschner.
Compositional generation for MC/DC test suites.
In Proceedings of TACoS'03, pages 1-11, 2003.
Electronic Notes in Theoretical Computer Science 82(6).
[RH01]: 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.
[RWN+98]: P. Raymond, D. Weber, X. Nicollin and N. Halbwachs.
Automatic Testing of Reactive Systems.
In Proc. 19th IEEE Real-Time Symposium, 1998.
[SPHP02]: 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.
[SV03]: M.I.A. Stoelinga and F.W. Vaandrager.
A testing scenario for probabilistic automata.
In Proc. ICALP '2003, $30^{th}$ International Colloquium on Automata, Lnaguages, and Programming, 2003.
to appear.
[SVD01]: Jan Springintveld, Frits Vaandrager, and Pedro R. D'Argenio.
Testing timed automata.
Theoretical Computer Science, 254(1-2):225-257, March 2001.
[TV92]: J. Tretmans and L. Verhaard.
A queue model relating synchronous and asynchronous communication.
In Proceedings of the $12^{th}$ International Conference on Protocol Specification, Testing and Verification. North-Holland, 1992.
[Wil01]: A. Wiles.
ETSI testing activities and the use of TTCN-3.
Lecture Notes in Computer Science, 2078:123-??, 2001.

Martin Leucker, July 01, 2003