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 consideres tools and techniques for formal verification of system designs. The course will integrate a CISS workshop day devoted to software validation techniques with focus on model-based testing. The last part of the course considers tools from control theory for modelling and simulating systems comprising both discrete and continuous parts. Particular emphasis will be put on hands-on application of validation tools including the real-time validation tool UPPAAL, UPPAAL Cora, "commercial" tools such as SPIN, visualSTATE, and tools for simulation such as Simulink and Ptolemy.
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 | Lecturer | Subject |
| 1 | November 12 | 8.30-12.00 | Kim Larsen, Gerd Behrmann |
Timed automata and Uppaal |
| 2 | November 15 | 8.30-12.00 | Kim Larsen, Gerd Behrmann |
Timed automata and Uppaal |
| 3 | November 19 | 8.30-15.00 |
Arne Skou, Theo Ruys |
SPIN |
| 4 | November 26 | 8.30-12.00 | Emmanuel Fleury | visualSTATE |
| 5 | December 1 | 9.00-16.00 | Tom Ball, Ed Brinskma, Klaus Havelund, Jens Grabowski |
CISS
seminar: Software Testing --Trends and Visions, |
| 6 | December 6 | 8.30-12.00 | Dan Bhanderi | Simulink, CheckMate |
| 7 | December 10 | 8.30-12.00 | Daniel Lazaro Cuadrado, John Knudsen |
Ptolemy, Rhapsody |
All lectures will take place in room E1-214, Fredrik Bajersvej 7, Building
E,
and start at 8.30.
Hands-on exercises (starting 10.15) will take place in PC-lab E1-110 also
Fredrik Bajersvej 7, Building E.
In order to pass the course you will need to solve a major modeling problem in on of the tools used in the course 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 Januaruy 7, 2005.
Take a look at this page for a long list of links about formal methods.