TCS / Studies / T-79.5303 Safety Critical Systems
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.5303 Safety Critical Systems (4 cr)

Spring 2007

This is a basic course on Safety Critical Systems and the use of Formal Methods to verify and validate safety systems. Subjects covered this year are: Requirement Engineering, Hazard/Risk Analysis Methods, System Reliability, Safety Critical Hardware/Software and Verification/Validation Tools. We will be particularly interested in the B-method for specification and verification (used by e.g. Airbus).

The course T-79.5303 replaces the earlier course T-79.232 Safety Critical Systems .

[Current] [General] [Lectures] [Tutorials] [Exams] [Material] [Feedback] [Links]


  • Course results have been input to TOPI on June 1.

General Information

  • The course consists of:
    • lectures (2 h per week, in English or Finnish depending on participants)
    • tutorials (1 h per week, English or Finnish, right after the lecture)
    • a compulsory home assignment

  • Registration for the course is by TOPI. You must register in order to take the course.

  • In order to pass the course you have to:
    1. pass the final home assignment


Lectures by Ilkka Herttua and Teemu Tynjala will take place on Thursdays from 1700 hrs to 1900 hrs in Computer Science building lecture room T4. The tutorials are held right after the lectures. They last at most one hour. Fear not -- most days, we will finish everything by 7 PM ;)

  • Jan. 18 (Ilkka Herttua & Teemu Tynjala) Introduction
  • Jan. 25 (Teemu Tynjala) Formal Methods - Introduction
  • Feb. 1 (Ilkka Herttua) Safety Critical Systems and Requirements Engineering
  • Feb. 8 (Ilkka Herttua) Risk Analysis and Safeware
  • Feb. 15 (Teemu Tynjala) B method - Basic Concepts
  • Feb. 22 (Ilkka Herttua) Formal Methods and Formal Specification
  • Mar. 1 (Teemu Tynjala) B method - Machine Consistency & Relations
  • Mar. 8 --- NO LECTURE
  • Mar. 15 (Ilkka Herttua) Verification, Validation & Testing
  • Mar. 22 (Teemu Tynjala) B method - Functions, Sequence & Nondeterminism
  • Mar. 29 (Ilkka Herttua) Tools and Applications
  • Apr. 5 ---- NO LECTURE
  • Apr. 12 (Teemu Tynjala) ProB - Model Checker for B language
  • Apr. 19 (Ilkka Herttua) Certification and standards -- THIS DATE WILL BE CHANGED

Ilkka's Lecture Slides

Teemu's Lecture Slides


Home Assignment

The compulsory home assignment needed to pass the course may be downloaded here: Assignment 2007.

The B machine Access needed in the assignment is here: Access.mch

The material related to Ilkka's questions is here (in jpg format. Save them on your disk and zoom in to read them):

Page 1 out of 3
Page 2 out of 3
Page 3 out of 3

You have until midnight May 11 to return the assignment. 50% of your grade will be determined by Ilkka's questions and the other 50% by my questions. Bonus from Ilkka's extra assignments will be counted to your benefit.

Good luck in the assignment!


We support two textbooks in the course:

Neil Storey: Safety Critical Systems
Nancy Leveson: Safeware

Both books cover the material necessary for completing the course.



[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 28 August 2007.