Formal Methods in Software Development (WS 2011/12)
Section outline
-
(KV3/Software Engineering: 326.013, KV4/Computer Mathematics: 326.053)
Time: Friday, 8:30-11:45.
Room: T 111.
Start: October 14, 2011.
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.
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.
-
Lectures in italics are mandatory for KV4 students but recommended also to KV3 students.
- October 14: introduction and organization, the language of logic.
- October 21: the art of proving, the RISC ProofNavigator.
- October 28: specifying and verifying (part 1).
- November 4: specifying and verifying (part 1).
- November 11: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 18: specifying and verifying (part 2).
- November 25: JML (part 1), ESC/Java 2.
- December 2: ESC/Java 2, the KeY verifier.
- December 9: JML (part 2).
- December 16: modeling concurrent systems.
- January 13: specifying in temporal logic (part 1), the Spin model checker.
- January 20: specifying in temporal logic (part 2).
- January 27: automatic model checking.
- February 3: Exam
-
- Computer Programs/Systems as Subject 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)
- Demonstration Examples
- Logic and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- An Axiomatic Basis for Computer Programming (restricted)
- Specifying and Verifying Programs: Part 2 (4 on 1)
- Invariant-based Programming
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- Extended Static Checking with ESC/Java 2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Specifying and Verifying Concurrent Systems
The password to this area is handed out in class.
-
The following software is used in this course (how to use the software):
- RISC ProofNavigator
- RISC ProgramExplorer
- 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.
- Documentation
- JML4c
- Extended Static Checking for Java (ESC/Java 2)
- KeY Verification Environment
- Spin Model Checker
-
10 exercises are handed out. 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 (in total 450 points have to be achieved).
The exercises have to be passed positively to be admitted to the exam.
-
The second exam takes place on
Thursday, March 29, 17:15-18:45, S2 Z74 (Science Park)
You have to register for the exam in KUSSS till Monday, March 26, 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.