There is a strong need for the use of advanced, systematic
techniques
and tools that support the system validation
process. [
Klaus Havelund ]
Software is becoming increasingly complex and there is a growing awareness within software engineering practice that both formal verification techniques as well as testing techniques are needed in order to deal with this growing complexity. This is in particular true in areas such as embedded systems used in consumer electronics, time dependent systems occurring in safety critical systems and communication protocols from the telecommunication industry. The focus of this course is on techniques and software-tools that can be used to assess the quality and correctness of software systems. The first part of the course considers tools and techniques for formal verification of system designs. The last part of the course considers tools and techniques for testing system implementations. Particular emphasis will be put on hands-on application of validation tools including the real-time validation tool UPPAAL, and "commercial" tools such as SPIN, visualSTATE and ESTEREL Studio.
The aim of the course is that the students become familiar with the possibility of validating software systems based on formal models and specifications (in particular of real-time and embedded systems) with the aid of software tools for the verification and analysis.
The schedule will be revised over the time of the course and more material will be added. Lectures will be held at Frb.7. We will move to E1-110 (PC-Lab) for excercises.
| No. | Lecture date | Time | Place | Lecturer | Subject |
| 1 | October 31st, 2003 | 8.30-10.30 10.30-12.00 |
B2-213 PC-Lab, E1-110 |
Kim and Gerd | Timed automata and Uppaal |
| 2 | November 7th, 2003 | 8.30-12.00 | E1-214 | Kim and Gerd | Timed automata and Uppaal |
| 3 | November 14th, 2003 | 8.30-12.00 13.00-14.00 |
E1-214 | Emmanuel Fleury Henrik Leerberg |
Intro to visualSTATE Guest lecture about visualSTATE |
| 4 | December 5th, 2003 | 8.30-15.00 | E1-214 | Theo Ruys | Spin |
| 5 | December 12th, 2003 | 8.30-12.00 | E1-214 | Daniel Lazaro Cuadrado Juhan Ernits |
Ptolemy |
In order to pass the course you will need to solve a major modeling problem in UPPAAL and hand in a small report documenting your model. We will present the problem during the third lecture. The deadline for handing in the report is the 5th of December, 2003.
Take a look at this page for a long list of links about formal methods.