Formal Methods in Software Development (WS 2016/17)
Section outline
-
Friday 8:30-11:45, Room: S2 053, Start: October 7, 2016
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 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.
-
The schedule is tentative and may be modified.
Lectures in italics are mandatory for KV4 students but also strongly recommended to KV3 students.
- October 7: introduction and organization, logic and proving.
- October 14: the RISC ProofNavigator, specifying and verifying (part 1).
- October 21: specifying and verifying (part 2).
- October 28: specifying and verifying (part 3), the RISC ProgramExplorer.
- November 4: the RISC ProgramExplorer.
- November 11: exponential distribution and its properties, poisson process, Markov chains, etc. (Sztrik).
- November 15 (15:30-18:45, S2 Z74): Markov-type queueing systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations. (Sztrik).
- November 18: modeling tools, retrial queueing systems, case studies. (Sztrik).
- November 25: JML (part 1), ESC/Java2.
- December 2: ESC/Java2, the Key Verifier.
- December 9: JML (part 2), modeling concurrent systems.
- December 16: specifying in temporal logic.
- January 13: the Spin model checker.
- January 20: 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)
- 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 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.
- Second Exam: Wednesday, March 29, 2017, 17:15-18:45, S3 048
- You have to register for the exam in KUSSS from March 1 to March 28, 12:00.
- All written (no electronic) materials are allowed.
- Second Exam: Wednesday, March 29, 2017, 17:15-18:45, S3 048