Formal Methods in Software Development (WS 2014/15)
Section outline
-
Friday, 8:30-11:45, S2 054 (Monday, November 10: 15:30-18:45, S2 120), Start: October 10, 2014
Important: To take part in the course, you have to enrol in the KUSSS system.The course is offered simultaneously as
- 326.013/KV3 (for the master program "Software Engineering") and
- 326.053/KV4 (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 News 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 10: introduction and organization, logic and proving.
- October 17: the RISC ProofNavigator, specifying and verifying (part 1).
- October 24: specifying and verifying (part 2).
- October 31: specifying and verifying (part 3), the RISC ProgramExplorer.
- November 7: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 10: Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 14: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 21: the RISC ProgramExplorer.
- November 28: JML (part 1), ESC/Java2.
- December 5: ESC/Java2, the Key Verifier.
- December 19: JML (part 2), modeling concurrent systems.
- January 16: specifying in temporal logic.
- January 23: the Spin model checker.
- January 30: automatic model checking.
-
- 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)
- 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 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
- 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 8 are used for grading (in total 400 points have to be achieved, 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 19 2015, 17:15-18:45, S2 046
- Registration in KUSSS by Monday, March 16 2015, 12:00.
- All written materials are allowed.
- 2nd Exam: Thursday, March 19 2015, 17:15-18:45, S2 046