Available in English only!

 

2G1516

Formal Methods Formella Metoder

 

Dept. of Microelectronics and Information Technology

 

NEWS – ABOUT THE COURSE – COURSE PM – REQUIREMENTS – SCHEDULE AND SLIDES –STAFF – SOURCE CODE –TOOLS – LITERATURE AND LINKS – HOWTO – MAILING LIST

News:

• 040205: We are scheduling a reexamination during week 11, March 8-12. Proposal is Wednesday 10, 8-13. Let us know quickly if you wish to attend but have problems with the time. Location will be Forum, Kista.

Check also the mailing list archive.

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 four main and complementary schools in the formal methods area, namely, theorem proving, model checking, Hoare logic and weakest precondition calculus, and process algebra.

 

The course consists of lectures, exercise sessions, labs, and a final exam. Lectures and exercise sessions are held on the main campus. 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:

Three labs (2 pts total), final exam (5 hours, 2 pts), activity, including take-home exam (1 pt). Final grade (U, 3, 4, 5) is determined by grade of final exam.

 

Labs and exercises can be done in teams of 2 or 3, not more, 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. Copying of solutions between teams is unethical behaviour, it will be discovered, and the entire team will fail the course if you decide to try.

 

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.

 

We have introduced the activity requirement to encourage discussion and activity, to increase depth of understanding, and to give you an opportunity to practice your presentation skills. The activity requirement has two components: Presence and general activity, and on one or two occasions (depending on how much work is involved) to lead discussion on a selected exercise. There is scope for negotiation on this last element – for instance we may agree to skip to presentations in favour of a paper presentation. We will agree on a schedule for exercise/paper presentations as we go along.

Schedule and Slides:

This is close-to-final version. Please keep up-to-date – schedule is prone to changes

 

During the first week of course you’ll be required to read, on your own, chapters 1-3 of Peled. At lecture 3, 3 Nov, a small take-home exam will be handed out on this material to be returned at lecture 4.

 

Activity	Time	Place	Subject	Reading	Lecturer	Todo
Lecture 1	27 Oct, 10-12	E51	Introduction (slides), modelling software systems (slides)	Peled ch 4	Dam
Exercise 1	28 Oct, 10-12	K53	Logic primer	Peled ch 1-3	Giambiagi
Lecture 2	30 Oct, 15-17	E51	Temporal logic (slides, 1-16)	Peled ch 5	Dam
Exercise 2	31 Oct, 13-15	K51	FOL (= First Order Logic) exercises		Giambiagi	Set #1: 1.5, 4, 6.2, 6.4, 8.3, 8.4
Lecture 3	3 Nov, 10-12	E51	LTL vs. CTL. Automata on infinite words (slides, 16-27)	Peled 5.5-onwards	Dam	FOL take-home exam handed out
Exercise 3	3 Nov, 13-15	E51	FOL + PVS exercises		Giambiagi	Set #1: 10.3, 11, 13, 16, 17.
Lecture 4	6 Nov, 15-17	K53	The automata framework (slides)	Peled Ch. 6	Dam	Take-home exam returned
Exercise 4	7 Nov, 13-15	K51	System modelling Intro to SPIN (slides)	Holtzmann Ch. 5 and Ch. 6. SPIN warm-up and lab assignment	Giambiagi
Lecture 5	10 Nov, 10-12	K53	LTL -> Automata (slides). Correctness and concurrency in SPIN (slides)	Holtzmann Ch. 8 and Ch. 11.	Dam
Exercise 5	10 Nov, 13-15	K52	Temporal Logic Automata exercises		Giambiagi	Set #2: 3, 5. Set #3: 1,4,5,8.
Lecture 6	17 Nov, 10-12	E51	Floyd/Hoare logic (slides)	Peled 7-7.5	Dam
Exercise 6	17 Nov, 13-15	E51	Automata exercises		Giambiagi	Set #4: 2,4.5,6,7.
Lab 1	20 Nov, 13-15	Karmosin, E-building, 5th floor	SPIN			Lab presentations (schedule)
Lecture 7	24 Nov, 10-12	E51	Owicki-Gries (slides), ESC/Java (slides)	Detlefs et al: Extended Static Checking	Dam
Exercise 7	24 Nov, 13-15	E51	Floyd/Hoare logic ESC/Java	ESC/Java lab assignment	Giambiagi
Lecture 8	27 Nov, 15-17	E51	CCS, syntax, semantics (slides)	Peled 8-8.6	Dam
Exercise 8	28 Nov, 13-15	K51	Owicki-Gries, weakest preconditions		Giambiagi	Set #5: 1, 6, 10.
Lecture 9	1 Dec, 10-12	E51	CCS, syntax, semantics (cont.)	Peled 8-8.6	Dam
Lab 2	1 Dec, 13-15	Karmosin, E-building, 5th floor	ESC/Java		Giambiagi	Lab presentations (schedule)
Lecture 10	4 Dec, 15-17	E51	CCS, process algebra (slides)	Rest of Ch. 8	Dam
Exercise 9	5 Dec, 13-15	K51	CCS exercises	CWB lab assignment	Giambiagi	Set #6:1-4.
Lecture 11	8 Dec, 10-12	E51	Mu-calculus (slides)		Dam
Exercise 10	8 Dec, 13-15	E53	CCS/mu-calculus		Giambiagi	Set #7
Lecture 12	9 Dec, 13-15	K51	Mu-calculus		Dam
Exercise 11	9 Dec, 15-17	K51	Consultations		Giambiagi
Lab 3	10 Dec, 13-15	Karmosin, E-building, 5th floor	CWB lab			Lab presentations (schedule)
Exam	18 Dec, 8-13	Q11	Questions (ps, pdf).			Reference solutions (ps, pdf).
Lab 4	28 Jan, 13-17	Karmosin, E-building, 5th floor	Re-evaluation of lab assignments			Schedule to be announced (mail your preferences)

 

 

Lab assistance

 

Pablo Giambiagi is available after the relevant exercise sessions for questions concerning labs

Staff:

Lecturer, course responsible:

Mads Dam, email: mfd at imit.kth.se, phone: 790 4123, mobile: 070 543 6787

Course assistant:

Pablo Giambiagi, email: pablo at kth.se, phone: 08 633 1588

Course Committee:

Mikael Lagerkvist (d00-mla at d.kth.se)

Kristoffer Sundström (kiffe at kth.se)

• 031201: First meeting (minutes).

Source Code:

• Alternating Bit Protocol in PROMELA
• Mobile IP Basic Model in PROMELA
• Priority Queues in Java
• Priority Queues (of integers) in Java

Tools:

• The Spin Model Checker ( installation instructions )
• The PVS Specification and Verification System
• ESC/Java: Extended Static Checking for Java
  If you experience problems with ESC/Java, it may be that it is incompatible with your version of Java. Check Task 3 in the ESC/Java lab assignment for hints on how to get around this problem.
• The Edinburgh Concurrency Workbench
  Here is a patched CWB 7.1 (Linux gzipped executable, Solaris gzipped executable) that produces the correct answer to the first command on p. 15 of the "CWB Workout."

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

Literature and Links:

• Course book is D. Peled: Software Reliability Methods, Springer-Verlag 2001. The book has been ordered to Kårbokhandeln both at Campus and in Kista (Electrum). Price is 550sek.
• Slides are published here. These are essential reading material for all lectures.
• Gerard J. Holtzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.

Howto:

• Register: Send an email to "pablo at kth.se"
• Install CWB (the Concurrency Workbench): Download the standalone executable that corresponds to your architecture, Linux or Solaris. Then follow the instructions here.
  We recommend that you use Emacs to edit your CWB sources. If you do so, we also recommend that you install the corresponding Emacs CWB mode.
  OBS: It is possible, in principle, to install CWB under Windows, but be warned that it is not that easy. To start with, you'll need a running SML system (SML/NJ has a Windows port but there are other options too). Then, you should try using any of the heap images supplied here. If this does not work, then go get a custom build file and follow the instructions therein.
• Hints on installing and using PVS, as well as on the PVS exercise (Set 1, Exercise 17) can be found here.
• Run Spin, ESC/Java and CWB on NADA computers: add the modules spin/4.0.7, escjava/1.2.4 and cwb/7.1, respectively.

Previous Exams:

• 031218: Questions (ps, pdf) & reference solutions (ps, pdf).

Mailing list:

We have set up a mailing list for general notifications among students and staff. Its address is "2G1516-formal-methods at it.kth.se". 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.