Formal Methods in Software Development (WS 2008/09)
Topic outline
-
Formal Methods in Software Development (WS 2008/09)
(KV4/computer mathematics: 326.053, KV3/software engineering: 326.013)
Time:
- Friday 8:30-11:45 (no lecture on January 23).
- Monday, November 10, 15:30-18:45 (HS 13, HS 14).
Start: October 10.
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.
- queueing theory and its application to the performance analysis of computing systems.
- 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.
To take part in the course, you have to enrol in the KUSSS system. 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.
- Friday 8:30-11:45 (no lecture on January 23).
-
Contents
- Computer Programs/Systems as Subjects of Formal Reasoning (Schreiner)
- Introduction (4 on 1)
- Fehler im System: der Traum von Software ohne Bugs (restricted)
- The Language of Logic (4 on 1)
- Specifying and Verifying Sequential Programs (Schreiner)
- Hoare Calculus and Predicate Transformers (4 on 1)
- An Axiomatic Basis for Computer Programming (restricted)
- Specifying and Verifying Java Programs (Schreiner)
- The Java Modeling Language: Part 1 (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Proof of Correctness of Data Representations (restricted)
- Extended Static Checking with ESC/Java2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- Specifying and Verifying Concurrent Systems (Schreiner)
- Queueing Theory and Its Applications (Sztrik)
Restricted Area
The password to this area is handed out in class. - Computer Programs/Systems as Subjects of Formal Reasoning (Schreiner)
-
Schedule
- October 10: introduction, logic, RISC ProofNavigator.
- October 17: RISC ProofNavigator, Hoare calculus.
- October 24: Hoare calculus, verification with RISC ProofNavigator.
- October 31 (T111!): Hoare calculus, verification with RISC ProofNavigator.
- November 7 (KV4): Queuing theory and its applications (Sztrik).
- November 10 (KV4, HS13/HS14): Queuing theory and its applications (Sztrik).
- November 14 (KV4): Queuing theory and its applications (Sztrik).
- November 21: JML (part 1), ESC/Java2.
- November 28: ESC/Java2, KeY.
- December 5: JML (part 2).
- December 12: modeling concurrent systems, simulating with Spin.
- December 19: specifying concurrent systems.
- January 9: model checking concurrent systems with Spin.
- January 16: verifying concurrent systems with the RISC ProofNavigator.
- January 30: exam.
- October 10: introduction, logic, RISC ProofNavigator.
-
Software
The following software is used in the course (see the instructions for the use of the course software):- RISC ProofNavigator
- 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.
- Extended Static Checking for Java (ESC/Java2)
- KeY Verification Environment
- Spin Model Checker
- RISC ProofNavigator
-
Exercises
10 exercises are handed out which account for 50% of the course grade.
- KV3 students have to elaborate at least 6 positively in due time,
- KV4 students have to elaborate at least 8 positively (at least 1 from the part of Prof. Sztrik) in due time.
- KV3 students have to elaborate at least 6 positively in due time,
-
Exam (2nd Chance)
The second exam takes place in written form on Tuesday, March 31, 17:15-18:45 in HS14. You have to register for the exam in the KUSSS system by Monday, March 30, 12:00. No materials are allowed; don't forget to bring your student id card with you. The exam has to be positively passed; it accounts for 50% of the course grade.