Formal Methods in Software Development (WS 2010/11)
Section outline
-
Formal Methods in Software Development (WS 2010/11)
(KV3/Software Engineering: 326.013, KV4/Computer Mathematics: 326.053)
Time: Friday 8:30-11:45.
Room: T 111 (November 10, 10:00-11:45: T 211)
Start: October 15.
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").
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.
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 Announcements forum and may yourself post messages in the Questions and Answers forum. - KV3/326.013 (for the master program "Software Engineering") and
-
Schedule
Lectures marked as "KV4" are mandatory for KV4 students but also recommended for KV3 students.- October 15: Introduction, the language of logic.
- October 22: RISC ProofNavigator, Hoare calculus.
- October 29: Hoare calculus, verification with the RISC ProofNavigator.
- November 5 (Sztrik): Exponential distribution and its properties, Poisson process, Markov Chains, etc.
- November 10 (Sztrik, T111+T211): Markov-type Queueing Systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations.
- November 12 (Sztrik): Modeling tools, Retrial Queueing Systems, Case Studies.
- November 19: Hoare calculus, verification with the RISC ProofNavigator.
- November 26: JML (part 1), ESC/Java2.
- December 3: ESC/Java2, KeY.
- December 10: JML (part 2).
- December 17: modeling concurrent systems, simulating with Spin.
- January 14: specifying concurrent systems.
- January 21: model checking concurrent systems with Spin.
- January 28: model checking, verifying concurrent systems with the RISC ProofNavigator.
- February 5: exam.
- October 15: Introduction, the language of logic.
-
Materials
- Computer Programs/Systems as Subjects 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)
- 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)
- Extended Static Checking with ESC/Java2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Specifying and Verifying Concurrent Systems
- Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
Restricted Area
The password to this area is handed out in class. - Computer Programs/Systems as Subjects of Formal Reasoning
-
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 (two by Prof. Sztrik). From these 10 exercises,
- KV3: the best 7 are used for grading (in total 350 points have to be achieved),
- KV4: the best 9 are used for grading (at least one must be from Prof. Sztrik; in total 450 points have to be achieved).
-
Second Exam
A second exam will take place on Thursday, March 31, 17:15-18:45 in BA 9912. You have to register in KUSSS for the exam (lecture number: 326.013) until Monday March 28, 12:00. No materials are allowed, do not forget to bring your student id with you. The exam must be passed positively; it accounts for 50% of the course grade.