Available in English only!
2G1516
Formal Methods
Formella Metoder

REPLACED BY 2D1452 FROM 06-07

 

05-06, Dept. of Microelectronics and Information Technology

NEWS - ABOUT THE COURSE - COURSE PM - REQUIREMENTS - SCHEDULE AND SLIDES -STAFF - HELP - SOURCE CODE -TOOLS - LITERATURE AND LINKS - HOWTO - PREVIOUS EXAMS -  MAILING LIST - PREVIOUS YEARS - COURSE EVALUATION

Using this page:

This is where to look for all information regarding 2G1516, autumn term 2005.  This page is updated frequently during term time so to not miss important information you'll need to check this page often.

News:

About the course:

See also handbook of studies.

Formal methods are about rigorous verification of systems. That is, techniques that can help bring about better confidence in the systems we develop and use, beyond what pure testing can achieve. This confidence is brought about, essentially, by analysis in terms of mathematics and logics. In the course we study some important tools and techniques that have been developed for this purpose, their foundations (i.e. how and why they work), and their applications to some concrete case studies (protocols and programs). Part of the message we want to get across is that this stuff can be actually really useful. During the course students will get exposed to three main approaches in the formal methods area, namely, model checking and temporal logic, Hoare logic and weakest precondition calculus, and process algebra.

The course consists of lectures, exercise sessions, labs, and a final exam. All sessions are given on the main campus, Valhallavägen. We have scheduled 12 double lectures and 12 double exercise sessions. Labs are to be done on whatever computer facilities you have available whether personal, at Campus, or at Forum. The only scheduled slots are to get your labs accepted. Make sure you start the labs as early as possible - in most cases not much prior knowledge is required to get started, and you'll want installation troubles and so forth out of the way well before the lab is due. Also the schedule is tight, and you will find it hard going to catch up once you're behind.

Course PM:

Is this document

Requirements:

Four labs (3 credits total), final exam (5 hours, 2 credits). Final grade (U, 3, 4, 5) is determined by grade of the final exam.
 
Labs and exercises can be done in teams of 2, or they can be done individually. Collaboration between teams is fine at the level of exchange of ideas, but each team must do its own work and is responsible for the correctness and originality of their results.
 
Each team must hand in a report explaining their solution, code, analysis results and conclusions. The report must be properly typed and written in understandable English by you. All text not written by you must be properly quoted. The report is handed to the course staff at the same time as the lab is demonstrated, at the scheduled slots.

Lab reports/presentations and the take-home exam are pass/fail, i.e. they must be produced at the scheduled time, with acceptable quality.

Schedule and Slides:

The official schedule is here. Locations are at Valhallavägen. This schedule applies as far as times and locations are concerned (except for locations for lab reporting, this will be announced). Changes to the official schedule are announced on this page.
 
Lectures and exercise sessions (but NOT the final exam) start quarter past. Links below get updated as the course moves on.

 
Activity
Time
Place
Subject
Reading
Lecturer
Todo
Lecture 1
27Oct, 10-12
L42
Introduction, Modelling software systems
Peled ch 4
Dam
Modelling Software Systems Exercises
Exercise 1
31 Oct, 13-15
 K53
Exercises and SPIN demo
Cohen
Lecture 2
1 Nov, 15-17
L44
Temporal logic
Peled ch 5. CTL part in slides not covered
Dam
 LTL exercises
Exercise 2
3 Nov, 10-12
L42
 Introduction to Promela and the Spin lab
 
Cohen
Promela Exercises, Spin Lab and Basic Mobile IP Model
Lecture 3
4 Nov, 10-12
L43
 Temporal logic cont'd; The automata framework Rest of Peled ch. 5; then start Peled ch. 6
Dam
Buchi automata exercises
Exercise 3
7 Nov, 13-15
K53
LTL and Buchi Exercises
Cohen
 
Lecture 4
 8 Nov, 15-17
L44
Correctness in SPIN
Holtzmann ch. 8 and 11. Peled ch 6
Dam
Automata framework + LTL translation exercises CTL exercises
Exercise 4
10 Nov, 10-12
L42
I
Cohen
 
Lecture 5
11 Nov, 10-12
L43
 LTL translation
 
Dam
 
Exercise 5
14 Nov, 13-15
K52
 
 
Cohen
Lab 2 reporting
15 Nov, 8-12 (?)
TBA
SPIN lab
-
Dam/Cohen
 
Lecture 6
16 Nov, 10-12
K51
Floyd/Hoare logic
 Peled ch 7-7,5
Dam
Floyd/Hoare logic exercises, Esc/Java Lab , Esc/Java Tutorial
Exercise 6 
17 Nov, 10-12
L42
 
Cohen
.
Lecture 7
18 Nov, 10-12
L43
Owicki-Gries, ESC/Java
Detlefs et al
Dam
 Finish Floyd/Hoare exercises
Exercise 7
21 Nov, 13-15
K52
 
 
Cohen
Lecture 8
 22 Nov, 15-17
L44
Finish Owicki-Gries,
Slides
Dam
Owicki-Gries exercises
Lab 4 reporting
23 Nov, 8-12 (?)
TBA
ESC/Java
-
Dam/Cohen
 
Exercise 8
24 Nov, 10-12
L42
 
 
Cohen
 
Lecture 9
25 Nov, 10-12
L43
 CCS, introduction
Peled 8-8.2, CCS paper
Dam
CCS Exercises CCS Lab
Exercise 9
28 Nov, 13-15
K52
CANCELLED
Cohen
Lecture 10
29 Nov, 15-17
L41
CCS, bisimulation equivalence
 Peled 8.5
Dam
Continue last set
Exercise 10
 1 Dec, 10-12
L42
CANCELLED
Cohen
Lecture 11
2 Dec, 10-12
L43
 CCS, examples, partition refinement
 
Dam
More CCS exercises
Exercise 11
 5 Dec, 13-15
K52
 
Cohen
Lecture 12
 6 Dec, 15-17
L44
CCS, modal logic, wrapping up, formal methods in industry
 
Dam
 
Lab 4 reporting
 8 Dec, 13-17
TBA
CCS/CWB
-
Dam/Cohen
 
Exercise 9 Dec, 13-15 L44 EXTRA TUTORIAL   Cohen  
Exam
 20 Dec, 14-19
D41
 
 

 

Labs

There are three labs in the course:

Expect that each lab will take you 2-3 working days. You are free to do the labs where it suits you, on own laptops, or in some of the machine halls at Campus or at Forum. Most tools are preinstalled in Stacken. Generally the tools presuppose general c.s.  literacy, including unix/linux and emacs.

Staff:

Lecturer, course responsible:

   Mads Dam, email: mfd at kth.se, phone: 790 4123, mobile: 0708 76 44 40

Course assistants:

    Mika Cohen, email mikac at imit.kth.se, phone: 790 4265, office: 8th floor, Forum building,elevator C. 

Help:

The course assistants can help you with the exercises and labs. In the first instance, you should try sending your question to the course mailing list.

Course Committee:

Source Code:

Tools:

For other tools, not used in this course, take a look at this page.

Literature and Links:

Howto:

Previous Exams:

Mailing list:

We have set up a mailing list for general notifications among students and staff. Its address is "formal-methods at imit.kth.se". You can find information on how to join the mailing list here. All mails sent to this list are stored in the list archive.
You can use the mailing list to share a question/comment that may be of interest to other students. Please, use the list discretionally, i.e. avoid discussing personal issues or matters outside the subject of this course. 

Previous years:

04-05, 03-04, predecessor course 2G1301

Course evaluation:

Here

Last edited: Mads on 060609