| | | Formal Methods in Software Development (WS 2009/10)
(KV3: 326.013, KV4: 326.053)
Time: Friday 8:30-11:45.
Room: T111
Start: October 9.
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.
It is expected that a guest lecturer will present a special topic. 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 KV3 (for the master program "Software Engineering") and KV4 (for the master program "Computer Mathematics"). The detailed organization will be explained in class.
To take part in the course, you have to enrol in the KUSSS system (please make sure to enrol for KV3/326.013 or KV4/326.054, as required by your degree program). 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.
| | | | 1 | Contents
- Computer Programs/Systems as Subjects of Formal Reasoning
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Java Programs
- Specifying and Verifying Concurrent Systems
- Special Topic (to be announced)
Restricted Area
The password to this area is handed out in class. | 
| | | 2 |
Schedule
Lectures marked as "KV4" are mandatory for KV4 students, KV3 students are welcome.
- October 9: introduction, the language of logic.
- October 16: RISC ProofNavigator, Hoare calculus.
- October 23: Hoare calculus, verification with the RISC ProofNavigator.
- October 30 (KV4): More on Hoare calculus and verification.
- November 13: JML (part 1), ESC/Java2.
- November 20: ESC/Java2, KeY.
- November 27: JML (part 2).
- December 4: modeling concurrent systems, simulating with Spin.
- December 11: specifying concurrent systems.
- December 18: model checking concurrent systems with Spin.
- January 15 (KV4): verifying concurrent systems with the RISC ProofNavigator.
- January 22 (KV4): guest lecture cancelled, self study assignment instead.
- January 29: February 1: exam.
|
| | | 3 | |
| | | 4 | AlloyAlloy is a structural modelling language based on first-order logic, for expressing complex structural constraints and behaviour. The Alloy Analyzer is a constraint solver that provides fully automatic simulation and checking. Unlike a programming language, an Alloy model is declarative: it can describe the effect of a behaviour without giving its mechanism. This allows very succinct and partial models to be constructed and analyzed. It is similar in spirit to the formal specification languages Z, VDM, Larch, B, OBJ, etc, but, unlike all of these, is amenable to fully automatic analysis in the style of a model checker. (Source: FAQ)
|
| | | 5 | Exercises
10 exercises are handed out. Exercise 0 is mandatory for everyone. From the remaining exercises 1-9,
- KV3: the best 6 are graded (in total 350 points have to be achieved),
- KV4: the best 8 are graded (in total 450 points have to be achieved).
|
| | | 6 | Exam
A second exam will take place on Wednesday, March 24, 2010, 17:15-18:45, in T111. To take part in the exam, you have to register for the exam in the KUSSS system until Monday, March 22, 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.
|
| |
| Skip Calendar
| Mon |
Tue |
Wed |
Thu |
Fri |
Sat |
Sun |
|---|
| 1 |
2 |
3 |
4 |
5 |
6 |
7 |
| 8 |
9 |
10 |
11 |
Today Friday, 12 March 12 |
13 |
14 |
| 15 |
16 |
17 |
18 |
19 |
20 |
21 |
| 22 |
23 |
24 |
25 |
26 |
27 |
28 |
| 29 |
30 |
31 |
| | | |
Events Key There are no upcoming events
25 Feb, 10:44 Wolfgang Schreiner Second Exam: Wednesday, March 24, 2010 more... 27 Jan, 15:06 Wolfgang Schreiner 13 Jan, 19:26 Wolfgang Schreiner Slide Set "Verifying Concurrent Systems" more... 13 Jan, 15:28 Wolfgang Schreiner January 22: guest lecture cancelled, self study assignment instead more... 21 Dec, 10:33 Wolfgang Schreiner Exam: February 1, 8:30-10:00, HS5 more...
|
