Formal Methods in Software Development (WS 2017/18)
Section outline
-
Friday 8:30-11:45, Room: S2 053, Start: October 6, 2017
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 "Computer Science") and
- KV4/326.053 (for the master program "Computer Mathematics").
Please 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.
-
The schedule is tentative and may be modified.
Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 6: introduction and organization, the language of logic, the RISC Algorithm Language.
- October 13: the art of proving, the RISC ProofNavigator, specifying and verifying (part 1).
- October 20: specifying and verifying (part 1).
- October 27: specifying and verifying (part 1), the RISC ProgramExplorer.
- November 3: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 7, 16:15-19:45, S2 120: Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 10: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 17: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 24: JML (part 1), ESC/Java2.
- December 1: ESC/Java2, the Key Verifier.
- December 15: JML (part 2), modeling concurrent systems.
- January 12: specifying in temporal logic.
- January 19: the Spin model checker.
- January 26: automatic model checking, verifying safety properties by computer-supported proving.
- October 6: introduction and organization, the language of logic, the RISC Algorithm Language.
-
- 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, Checking, and Proving (4 on 1)
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Programs: Part 1 (4 on 1)
- Specifying and Verifying Programs: Part 2 (4 on 1)
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- Behavioral Interface Specification Languages (restricted)
- Specification and Verification: The Spec# Experience (restricted)
- 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)
- Proof of Correctness of Data Representations (restricted)
- Formal Verification of Object-Oriented Software (COST Action IC0701)
- Demonstration Examples
- Specifying and Verifying Concurrent Systems
- Modeling Concurrent Systems (4 on 1)
- Specifying and Verifying System Properties (4 on 1)
- Model-Checking Concurrent Systems (4 on 1)
- Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
- Talking Model Checking Technology (restricted)
- ClientServer.txt
- Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
- Announcement
- Lecture Notes of Janos Sztrik
- Queueing Theory Books Online
- Java Applets for Queueing Theory
The password to this area is handed out in class.
-
The following software is used in this course (how to use the software):
- RISC Algorithm Language
- 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
- OpenJML
- Extended Static Checking for Java (ESC/Java 2)
- KeY Verification Environment
- Tutorial (local copy), More Tutorials and Examples
- 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 earned),
- KV4: the best 8 are used for grading (in total 400 points have to be earned, 1 exercise must be from the part of Sztrik).
-
The final exam must be passed positively; it accounts for 50% of the course grade.
- Second Exam: Tuesday, April 10, 17:15-18:45, S2 019.
- Registration in KUSSS (all participants for course 326.013) required till April 9 12:00.
- All written (no electronic) materials are allowed.
- Second Exam: Tuesday, April 10, 17:15-18:45, S2 019.