[Contact]
[Schedule]
[Meetings]
[Participants]
[Topics]
Graduate Reading Course on Formal Software Testing and Model Checking
Contact
For questions, please contact
Anders Hessel,
Paul Pettersson,
Martin Leucker,
or
Bengt Jonsson.
E-mail:
{
hessel,
paupet,
leucker,
bengt
}@it.uu.se
Schedule
(Subject to change).
| Date:
| Time:
| Weekday:
| Title:
| Link:
| Presenter:
|
| 2002-09-24
| 13.15 -15.00
| Tuesday
| Intoduction, Survey
| (to the meeting)
| Martin Leucker
|
| 2002-09-30
| 13.15 -15.00
| Monday
| Guest speaker from industry
| (to the meeting)
| Antti Huima, Conformiq
|
| 2002-10-04
| 13.15-15.00
| Friday
| Principle and Methods of Testing FSM -A Survey
| (to the meeting)
| Olga Grinchtein
|
| 2002-10-10
| 10.15-12.00
| Thursday
| Adaptive Model Checking
| (to the meeting)
| Martin Leucker
|
| 2002-10-18
| 10.15-12.00
| Friday
| Test Case Generation
| (to the meeting)
| Rafal Somla
|
| 2002-10-24
| 10.15-12.00
| Thursday
| SDL and Test Case Generation
| (to the meeting)
| Anders Hessel
|
| 2002-11-07
| 10.15-12.00
| Thursday
| TTCN-3 ...
| (to the meeting)
| Tobias Amnell
|
| 2002-11-15
| 10.15-12.00
| Friday
| Verification of Test Suites
| (to the meeting)
| Therese Berg
|
| 2002-11-22
| 10.15-12.00
| Friday
| Generating Test Cases for a Timed I/O Automaton Model
| (to the meeting)
| Leonid Mokrushin
|
| 2002-11-29
| 13.15-15.00
| Friday
| Startegies for Conformance Testing
| (to the meeting)
| Martin Leucker
|
| 2002-12-05
| 10.15-12.00
| Thursday
| Alternating-time Temporal Logic
| (to the meeting)
| Mayank Saksena
|
| 2002-12-12
| 10.15-12.00
| Thursday
| Minimum-cost solutions for testing protocols with timers etc.
| (to the meeting)
| Oskar Wibling
|
| 2002-12-19
| 10.15-12.00
| Thursday
| Projected state machine coverage
| (to the meeting)
| Johan Blom
|
| Merry
| Christmas
| and
| a
| Happy
| New Year
|
Meetings
Articles should have been read before the meeting,
the articles are listed in decreasing importance.
Meetings will be held weekly, at Thursdays 10.15-12.00 in room 1406.
More meetings will be annonced.
Introduction
Date : 2002-09-24
Time : 13.15 -15.00
Room : 1406
Presenter: Martin Leucker
Formal Conformance Testing and Data-Intensive Timed Systems: From Foundations to Industrial Relevancy
Date : 2002-09-30
Time : 13.15 -15.00
Room : 2145
Title: Formal Conformance Testing and Data-Intensive Timed Systems:
From Foundations to Industrial Relevancy
Presenter: Antti Heima, Conformiq Software Ltd.
|
ABSTRACT: Applying the ideas of formal conformance testing to
industrial problems is all but straightforward, most notably because
real-world systems are (1) data-intensive, (2) timed, and (3)
infinite-state. In this talk we consider the research focus points of
Conformiq and what we perceive to be the fundamental problems on the
current theoretical frontier. This is a position-talk type.
presentation. No deep abstract theories will be presented; so everyone
interested in this field is warmly welcome. Topics touched: symbolic
& abstraction methods, timed systems, measuring black-box testing
coverage.
|
|
ABOUT THE AUTHOR: Mr. Antti Huima (M.Sc. Tech) works as the Chief
Scientific Officer for Conformiq Software Ltd, a Finnish SME focusing
on developing an industrial-strength product for automatic formal
conformance testing. Mr. Huima is also a post-graduate student at the
Laboratory for Theoretical Computer Science at Helsinki Univ of Tech,
preparing his PhD thesis on the formal verification of computer
programs with unbounded heap-structured memory. This Autumn Mr. Huima
gives also a class at HUT on formal conformance testing, aimed at
3rd-4th year M.Sc.-students majoring in CS.
|
Principle and Methods of Testing FSM -A Survey
Date : 2002-10-04
Time : 13.15 -15.00
Room : 1406
Presenter: Olga Grinchtein
- David Lee and Mihalis Yannakakis
Principles and methods of testing finite state machines -A survey
The Proceedings of the IEEE,
84, August 1996,
pdf.
The presentation can be downloaded here (ps).
Adaptive Model Checking
Date : 2002-10-10
Time : 10.15 -12.00
Room : 1406
Presenter: Martin Leucker
- D. Peled and M. Vardi and M. Yannakakis"
Black Box Checking,
Proc. FORTE/PSTV, Kluwer,
pages 225-240, 1999.
The document
at Rice, local (ps).
- Alex Groce and Doron Peled and Mihalis Yannakakis
Adaptive Model Checking,
Lecture Notes in Computer Science,
Volume 2280, pages 357--??, 2002.
The document local (pdf).
The presentation can be downloaded here (ps),
or here (pdf).
Test Case Generation
Date : 2002-10-18
Time : 10.15 -12.00
Room : 1406
Presenter: Rafal Somla
We wait until Monday 14th so Rafal can agree on the paper...
- Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, and Hasan Ural
A Temporal Logic Based Theory of Test Coverage and Generation
J,-P. Katoen and P. Stevens (Eds.): TACAS 2002, LNCS 2280,
pp. 327-341, 2002.
Springer-Verlag Berlin Heidelberg 2002
The document at Springer (pdf) and local (pdf)
The presentation can be downloaded here (ps),
SDL and Test Case Generation
Date : 2002-10-24
Time : 10.15 -12.00
Room : 1406
Presenter: Anders Hessel
A presentation of SDL
and
- C. Bourhfir, E. Aboulhamid, R, Dssouli, and N. Rico
A test case generation approach for conformance testing of SDL systems
Computer Communications, vol. 24,
pp. 319-333, March/April 2001
The document at Universite de Montreal (pdf) and local (pdf).
The presentation can be downloaded here (ps).
The slides for SDL where taken from Anders Hessel's master thesis presentation at ARTES summer school 2002.
TTCN-3 session
Date : 2002-11-07
Time : 10.15 -12.00
Room : 1406
Presenter: Tobias Amrell
A presentation of TTCN-3 ..
-
Jens Grabowski, Anthony Wiles, Colin Willcock, Dieter Hogrefe
On the Design of the new Testing Language TTCN-3 .
13th IFIP International Workshop on Testing Communicating Systems' (Testcom 2000), Ottawa, 29.8.2000-1.9.2000,
Kluwer Academic Publishers, August
2000.
here(pdf)
Original link to FOCUS here
- Anthony Wiles, ETSI, France
Theofanis Vassiliou-Gioles, Testing Technologies, Germany
Scott Moseley, FSCOM, France
Sebastian Mueller, FSCOM, France
Other Contributors
Frederique Aurouet, ACACIA, France
Csaba Koppany, Ericsson, Hungary
Experiences of Using TTCN-3 for Testing SIP and OSP
Whitepaper from www.etsi.org/tiphonweb/
here (pdf)
Original link to ETSI here (pdf)
Verification of Test Suites
Date : 2002-11-15
Time : 10.15 -12.00
Room : 1406
Presenter: Therese Berg
A presentation of the paper
- Claude Jard, Thierry Jeron, and Pierre Morel
Verification of Test Suites
Testing of communication systems,
IFIP TC6/WG6.1 13th International Conference on Testing of Communicating
Systems (TestCom 2000), August 29 -September 1, 2000, Ottawa, Canada. Ed.
Hasan Ural, Robert L. Probert, Gregor v. Bochmann
Boston[u.a]: Kluwer Academic
Copies will be distributed by hand.
Generating Test Cases with Timed Automaton
Date : 2002-11-22
Time : 10.15 -12.00
Room : 6002
Presenter: Leonid Mokrushin
A presentation of the paper:
The presentation can be downloaded here (ps),
or here (ppt).
Strategies for Conformance Testing
Date : 2002-11-29
Time : 13.15 -15.00
Room : 1406
Discussion leader: Martin Leucker
A presentation of the paper:
- Ramangalahy, Solofo,
Strategies for Conformance Testing
Max-Planck-Institut für Informatik,
Stadtwald, D-66123 Saarbrücken, Germany,
MPI-I-98-2-010, May,
1998,
0946-011X
The document can be downloaded at Max-Planck-Institut für Informatik,
or local copy here (ps) .
Alternating-time Temporal Logic
Date : 2002-12-05
Time : 10.15 - 12.00
Room :
Presenter: Mayank Saksena
A presentation of the paper:
Minimum-cost solutions for testing protocols with timers
Date : 2002-12-12
Time : 10.15 - 12.00
Room : 1406???
Presenter: Oskar Wibling
A presentation of the papers:
- M. Uyar and M. Fecko and A. Sethi and P. Amer
Minimum-cost solutions for testing protocols with timers
Tech. Rep. TR-97-17, CIS Dept., University
of Delaware, Newark, DE, 1997.
The document can be found at citeseer.nj.nec.com/article/23781.html
or local
(ps) and
(pdf).
- M.A. Fecko, M.U. Uyar, A.S. Sethi, P.D. Amer
Optimum Test Sequence Generation From Estelle Specifications
Proc. Int'l Workshop FDT Estelle, Evry, France, Nov 1998
The document can be found at citeseer.nj.nec.com/525728.html
or local
(ps) and
(pdf).
Projected state machine coverage
Date : 2002-12-19
Time : 10.15 - 12.00
Room : 1406
Presenter: Johan Blom
- Galit Friedman, Alan Hartman, Ken Nagin, and Tomer Shiran
Projected state machine coverage for software testing
Paper to appear in ISSTA 2002.
The document can be found at http://www.agedis.de/downloads.shtml
or local (pdf)
- David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang
Protocol Verification as a Hardware Design Aid
1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society, pp. 522-525.
The document can be found at http://sprout.stanford.edu/dill/murphi.html
or local (ps)
Additional reading
Some concrete examples are:
Participants
The following addresses can be contacted through "testing@hessel.nu".
| Name: | E-mail:
|
| Anders Hessel
|
| Bengt Jonsson
|
| Elena Fersman
|
| Gerardo Schneider
|
| Johan Blom
|
| Leonid Mokrushin
|
| Martin Leucker
|
| Mayank Saksena
|
| Olga Grinchtein
|
| Oskar Wibling
|
| Paul Pettersson
|
| Rafal Somla
|
| Therese Berg
|
| Tobias Amnell
|
Anders.Hessel@it.uu.se
Last modified: Fri Dec 13 13:24:46 MET 2002
