Course: Formal Methods in Software Development (WS 2007/08)

Enrol me in this course

	Formal Methods in Software Development (326.009/326.013, WS 2007/08) Time: Friday 8:30-11:45 (except October 19 and November 9) Friday 14:30-18:00 (additional classes on October 12 and November 16) Room: HS 11 (regular and additional class on November 16) HS 14 (additional class on October 12) Start: October 5. 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, proof-carrying code. 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. The course is offered simultaneously as 4KV (for the master program "computer mathematics") and 3KV (for the master program "software engineering"). The detailed organization will be explained in class. 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. News forum

1	Contents Computer Programs/Systems as Subjects of Formal Reasoning Introduction (4 on 1) Demonstration Examples Fehler im System: der Traum von Software ohne Bugs (restricted) The Language of Logic (4 on 1) Specifying and Verifying Sequential Programs Computer-Supported Program Verification with the RISC ProofNavigator (4 on 1) sum.pn, modus.pn, arrays2.pn, linsearch.pn Hoare Calculus and Predicate Transformers (4 on 1) An Axiomatic Basis for Computer Programming (restricted) Specifying and Verifying Java Programs The Java Modeling Language: Part 1 (4 on 1) The Java Modeling Language: Part 2 (4 on 1) Inststack.java, jml-examples.tgz 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 Modeling Concurrent Systems (4 on 1) Specifiying Properties of Concurrent Systems (4 on 1) Verifying Concurrent Systems (4 on 1) clientServer.txt, clientServer-mutex.ltl, clientServer-progress.ltl roads.txt, roads.ltl protocol.pn, clientServer.pn Abstrakte Kunst: Fehler finden durch Model Checker (restricted) Proof-Carrying Code (PCC) A class given by Hans-Wolfgang Loidl (LMU Munich), member of the EmBounded project and of the former Mobile Resource Guarantees project. Proof-carrying-code (PCC) is a software mechanism that allows a host system to determine with certainty that it is safe to execute a program supplied by an untrusted source. This is achieved by attaching a condensed version of a formal proof to the program. In this part of the course we will examine the principles of PCC, explore different variants in the design of a PCC infrastructure, and take a closer look at some selected PCC infrastructures. The structure of this part of the course is as follows: Motivation Basic Concepts An Example: CCured Components of the PCC Architecture Main challenges PCC for Resources Certificate Generation Summary Reading List Restricted Area The password to this area is handed out in class

2	Schedule October 5, 8:30-11:45 (all): introduction, logic, RISC ProofNavigator October 12, 8:30-11:45 (all): RISC ProofNavigator, Hoare calculus October 12, 14:30-18:00 (all): Hoare calculus, verification with RISC ProofNavigator November 16, 8:30-11:45 (all): JML, ESC/Java2 November 16, 14:30-18:00 (KV4 only): more on Hoare calculus and verification November 23, 8:30-11:45 (all): ESC/Java2, JML November 30, 8:30-11:45 (all): JML/KeY December 7, 8:30-11:45 (all): modeling concurrent systems, simulating with Spin December 14, 8:30-11:45 (all): specifying concurrent systems January 11, 8:30-11:45 (all): model checking with Spin January 18, 8:30-11:45 (KV4 only): modeling message passing, verification with the RISC ProofNavigator January 25, 8:30-11:45 (KV4 only): guest lecture on PCC by H.W. Loidl February 1, 8:30-10:00 (all): exam

3	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) Extended Static Checking for Java (ESC/Java2) ESC/Java2 needs Java 1.4.2, it does not work with Java 1.5! KeY Verification Environment Spin Model Checker

4	Exercises 8 exercises are handed out; at least 7 (KV3 students: 5) of them have to be positively elaborated within two weeks. The exercises account for 50% of the course grade. Exercise 1 (October 22) Assignment Exercise 2 (November 12) Assignment Exercise 3 (December 3) Assignment Exercise 4 (December 10, KV4 only) Assignment Exercise 5 (December 17) Assignment Exercise 6 (January 7; KV4 only) Assignment Exercise 7 (January 14) Assignment Exercise 8 (January 28) Assignment Exercise 9 (March 17) Assignment

5	Exam The final exam takes place in written form on Friday, February 1 2008, 8:30-10:00 in HS11. 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. Results Another exam will take place in April; check the course page at the beginning of March. 2nd Exam A second exam takes place in written form on Wednesday, April 2 2008, 17:15-18:45 in K009D. You have to register in KUSSS for the exam by April 1, 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.