Formal Methods in Software Development (WS 2018/19)
Section outline
-
Friday 8:30-11:45, S3 055, Start: October 5, 2018
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.
-
Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 5: introduction and organization, the language of logic, the RISC Algorithm Language.
- October 12: specifying and verifying (part 1).
- October 19: specifying and verifying (part 1).
- November 5 (10:15-13:30, S3 048): exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 7 (15:30-18:45, K 001A): Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 9: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 16: specifying and verifying (part 1), the art of proving, the RISC ProofNavigator,
- November 23: specifying and verifying (part 2), the RISC ProgramExplorer.
- November 30: JML (part 1), ESC/Java2.
- December 7: ESC/Java2, the Key Verifier.
- December 14: JML (part 2), modeling concurrent systems.
- January 11: specifying in temporal logic.
- January 18: the Spin model checker.
- January 25: automatic model checking, verifying safety properties by computer-supported proving.
- October 5: 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)
- Formally Verified Software in the Real World (restricted)
- Demonstration Examples
- Logic, Checking, 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)
- summation.txt, linsearch2.txt, linsearch3.zip
- 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)
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.
- 2nd Exam: Thursday, March 28, 2019, 17:15-18:45, S3 057.
- Mandatory Registration in KUSSS: March 3 to March 27, 12:00 (also KV4 participants register for 326.013 exam).
- All written (no electronic) materials are allowed.
- 2nd Exam: Thursday, March 28, 2019, 17:15-18:45, S3 057.