Methods and Tools for Validation
Modeling and Analysis
Dat5/F9D/SSE3, Fall 2002

1 Overview

In this Dat5/F9D course we cover a mixture of classical and emerging techniques and tools from the area of model-checking and testing, such as

• Timed Automata (UPPAAL)
• Linear Temporal Logic, Büchi Automata (SPIN)
• Computational Tree Logic (SMV)
• Partial Order Reduction, Symmetry Reduction (MURPHI)
• Probabilistic Models & Logics (Markov Chains, Markov Decision Processes, PCTL, MTBDDs) (PRISM, ETMCC, RAPTURE)
• SAT-based methods (CHAFF, PROVER)
• (Quantified) Propositional Logic, BDDs, BEDs (SMV, visualSTATE)
  

In addition to verification based on model-checking the course will focus on model-based testing including testing of finite-state machines (ordinary, timed or stochastic).

Part of the course will consist of student presentation (a total of 16) and additional presentations by myself (Kim G Larsen) and possible guest presenters. A high degree of interaction and frequent discussions will be encouraged. It is expected that you attend all sessions, read (and mostly understand) the papers for each session, and are able to pose "nasty" questions to the presenters about the papers. Note that it may in some cases, e.g., when presenting a paper yourself, be necessary to read additional papers referenced by your paper in order to fully understand your own paper.


Suggested literature (under the above given themes) can be found here.

2 Schedule

Lectures (and exercises) are scheduled Tuesdays 10:00 - 12:00, generally in E3-209 (deviations are indicated in the schedule). The schedule is at present only partial but will be completed during the course (thus, carefully observe the web-page).

3 Material & Links

• [JPK] Joost-Pieter Katoen: " Concepts, Algorithms, and Tools for Model Checking" . (Lecture Notes)
• [CPG] Clarke, Grumberg, Peled: Model Checking.
• [JPKnew] SPIN, SPIN slides, LTL , CTL .
• SPIN homepage .
• MUPHI homepage.
• Ed Clarke's homepage .
• Doron Peled's homepage .
• Moshe Vardi's homepage .
• SAT-live homepage .
• Fabio Somenzi homepage
• Marta Kwaitkowska homepage .
• Joost-Pieter Katoen homepage .
• Holger Hermanns homepage .
• John Hatclif homepage .
• Rajeev Alur homepage .
• Tom Henzinger homepage .
• UPPAAL homepage.
• RAPTURE homepage.

4 Presentation Hints (points to be discussed)

• The following is a list of hints for making more effective presentations. Note that the hints are not firm rules and should be adapted to the specific situation in which they are used. We will restructure and update the list during the course.
• Make sure that the presentation has a simple structure and that the listener understands and is able to follow the structure during the presentation. There should probably be an overview slide at the beginning and a talk summary/conclusions slide at the end. It may be useful to remind the listener of the structure during the presentation.
• It is often a good idea to divide a presentation into three separate parts. The first part should present the material without criticism, but be as faithfully to the authors as possible. The second part then relates the material to a) related work, e.g., as presented on DAT5 and b) your DAT5 project. The third part evaluates both form and content of the presented material, i.e., good and bad points. A self-evaluation of the presentation is also possible (not done at the exam). The time spent on these parts should be about 20, 5, and 5 minutes, respectively (give or take a few minutes), as this follows the DAT5 exam format.
• It is generally a good idea to mix general observations with concrete examples. It is often time-consuming and difficult to construct good, specific examples, but the time spent on this is well spent. Important observations that the listener should definitely understand are prime candidates for exemplification.
• Rehearse the presentation in front of an audience before the exam. It is important to actually say out loud all words of the presentation. Only this way is it possible to get a good feeling for the length of the talk and to identify trouble spots in the presenation that need further work.
• Make sure that the slides are easy to present. If some transitions between slides are difficult to remember then the slides should probably be revised. Again, the way to identify problems is through saying all the words out loud.
• Do number the slides; this makes it easier for the listeners to later refer to them.
• For the exam, it is a good idea to have everything on the slides so that there is no need to draw spontaneous pictures on the board.

It may be useful to have a look on the following papers on how to give good presentations:

• How to Present a paper in Theoretical Computer Science: A Speaker's Guide for Student.
• How to Give a Good Research Talk.

Kim G. Larsen (kgl@cs.auc.dk)