Course: Formal Methods in Software Development (WS 2010/11)

General

Formal Methods in Software Development (WS 2010/11)
(KV3/Software Engineering: 326.013, KV4/Computer Mathematics: 326.053)

Time: Friday 8:30-11:45.
Room: T 111 (November 10, 10:00-11:45: T 211)
Start: October 15.

Important: To take part in the course, you have to enrol in the KUSSS system. The course is offered simultaneously as

KV3/326.013 (for the master program "Software Engineering") and
KV4/326.053 (for the master program "Computer Mathematics").

Please make sure to enrol for the course intended for your degree program.

This course gives a survey on the use of formal methods for the development of reliable software. More specifically, we deal with

specifying sequential programs and concurrent systems,
computer-supported verification,
extended static checking,
model checking.

Furthermore, a guest lecture by Janos Sztrik (University of Debrecen) will give an introduction on

queueing theory and its application to the performance analysis of computing systems.

The course consists of two parts:

a lecture part where the fundamental issues of the field are taught, and
an exercise part where practical skills are trained using freely available software tools.

The grading of the course will be based on a couple of exercises and a final exam.

Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.

Questions and Answers Forum

Topic 1

Schedule

Lectures marked as "KV4" are mandatory for KV4 students but also recommended for KV3 students.

October 15: Introduction, the language of logic.
October 22: RISC ProofNavigator, Hoare calculus.
October 29: Hoare calculus, verification with the RISC ProofNavigator.
November 5 (Sztrik): Exponential distribution and its properties, Poisson process, Markov Chains, etc.
November 10 (Sztrik, T111+T211): Markov-type Queueing Systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations.
November 12 (Sztrik): Modeling tools, Retrial Queueing Systems, Case Studies.
November 19: Hoare calculus, verification with the RISC ProofNavigator.
November 26: JML (part 1), ESC/Java2.
December 3: ESC/Java2, KeY.
December 10: JML (part 2).
December 17: modeling concurrent systems, simulating with Spin.
January 14: specifying concurrent systems.
January 21: model checking concurrent systems with Spin.
January 28: model checking, verifying concurrent systems with the RISC ProofNavigator.
February 5: exam.

Topic 2

Materials

Computer Programs/Systems as Subjects of Formal Reasoning

Introduction (4 on 1)

Demonstration Examples

Fehler im System: der Traum von Software ohne Bugs (restricted)
Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
Formal Methods: Practice and Experience (local copy)

The Language of Logic (4 on 1)

Specifying and Verifying Sequential Programs

Hoare Calculus and Predicate Transformers (4 on 1 )

An Axiomatic Basis for Computer Programming (restricted)

Computer-Supported Program Verification with the RISC ProofNavigator (4 on 1)

Demonstration Examples

Specifying and Verifying Java Programs

Demonstration Examples

Verifying Java Programs with KeY (4 on 1)

The Java Modeling Language: Part 2 (4 on 1)

Specifying and Verifying Concurrent Systems

Modeling Concurrent Systems (4 on 1)

Demonstration Examples

Specifying Properties of Concurrent Systems (4 on 1)
Verifying Concurrent Systems (4 on 1)

Demonstration Examples

Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
Talking Model Checking Technology (restricted)

Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)

List of Queueing Theory Software

Restricted Area

The password to this area is handed out in class.

Topic 3

Software

The following software is used in the course (see the instructions for the use of the course software):

RISC ProofNavigator
Java Modeling Language (JML) Tools

Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.

Extended Static Checking for Java (ESC/Java2)
KeY Verification Environment
Spin Model Checker

Spin Online References

Topic 4

Exercises
10 exercises are handed out (two by Prof. Sztrik). From these 10 exercises,

KV3: the best 7 are used for grading (in total 350 points have to be achieved),
KV4: the best 9 are used for grading (at least one must be from Prof. Sztrik; in total 450 points have to be achieved).

The exercises have to be passed positively to be admitted to the exam.

Topic 5

Second Exam

A second exam will take place on Thursday, March 31, 17:15-18:45 in BA 9912. You have to register in KUSSS for the exam (lecture number: 326.013) until Monday March 28, 12:00. No materials are allowed, do not forget to bring your student id with you. The exam must be passed positively; it accounts for 50% of the course grade.