Formal Methods in Software Development (WS 2009/10)
Section outline
-
Formal Methods in Software Development (WS 2009/10)
(KV3: 326.013, KV4: 326.053)
Time: Friday 8:30-11:45.
Room: T111
Start: October 9.
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.
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.
To take part in the course, you have to enrol in the KUSSS system (please make sure to enrol for KV3/326.013 or KV4/326.054, as required by your degree program). 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 News forum.
- specifying sequential programs and concurrent systems,
-
Contents
- Computer Programs/Systems as Subjects of Formal Reasoning
- Introduction (4 on 1)
- 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)
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Proof of Correctness of Data Representations (restricted)
- Formal Verification of Object-Oriented Software
- Extended Static Checking with ESC/Java2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- Specifying and Verifying Concurrent Systems
- Special Topic (to be announced)
Restricted Area
The password to this area is handed out in class. - Computer Programs/Systems as Subjects of Formal Reasoning
-
Schedule
Lectures marked as "KV4" are mandatory for KV4 students, KV3 students are welcome.- October 9: introduction, the language of logic.
- October 16: RISC ProofNavigator, Hoare calculus.
- October 23: Hoare calculus, verification with the RISC ProofNavigator.
- October 30 (KV4): More on Hoare calculus and verification.
- November 13: JML (part 1), ESC/Java2.
- November 20: ESC/Java2, KeY.
- November 27: JML (part 2).
- December 4: modeling concurrent systems, simulating with Spin.
- December 11: specifying concurrent systems.
- December 18: model checking concurrent systems with Spin.
- January 15 (KV4): verifying concurrent systems with the RISC ProofNavigator.
- January 22 (KV4): guest lecture cancelled, self study assignment instead.
- January 29: February 1: exam.
- October 9: introduction, the language of logic.
-
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
- RISC ProofNavigator
-
Alloy
Alloy is a structural modelling language based on first-order logic, for expressing complex structural constraints and behaviour. The Alloy Analyzer is a constraint solver that provides fully automatic simulation and checking. Unlike a programming language, an Alloy model is declarative: it can describe the effect of a behaviour without giving its mechanism. This allows very succinct and partial models to be constructed and analyzed. It is similar in spirit to the formal specification languages Z, VDM, Larch, B, OBJ, etc, but, unlike all of these, is amenable to fully automatic analysis in the style of a model checker. (Source: FAQ)- Alloy Site (FAQ)
- Publications
- Alloy: A Lightweight Object Modelling Notation (original version of the language, now outdated)
- A Micromodularity Mechanism (revised version of the language)
- Formal Modeling and Analysis of a Flash Filesystem in Alloy
- Software Abstractions: Logic, Language, and Analysis
- Tutorial
-
Exercises
10 exercises are handed out. Exercise 0 is mandatory for everyone. From the remaining exercises 1-9,
- KV3: the best 6 are graded (in total 350 points have to be achieved),
- KV4: the best 8 are graded (in total 450 points have to be achieved).
-
Exam
A second exam will take place on Wednesday, March 24, 2010, 17:15-18:45, in T111. To take part in the exam, you have to register for the exam in the KUSSS system until Monday, March 22, 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.