Formal Methods in Software Development (WS 2007/08)
Section outline
-
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)
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.
- 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.
-
Contents
- Computer Programs/Systems as Subjects of Formal Reasoning
- 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
- 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)
- 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
The password to this area is handed out in class
-
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
- October 5, 8:30-11:45 (all): 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)
- 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
- RISC ProofNavigator
-
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. -
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.