Lecture "Formal Methods in Software Engineering"

Vorlesung "Formale Methoden der Softwareentwicklung"

July 2, 2007 - July 20, 2007

4.1.21 V2 c CV, In(KITE,ST) - Summer Academy

Jun.-Prof. Dr. Bernhard Beckert


This lecture is held within the Summer Academy 2007. It is part of the Software Engineering Module, which also contains the lecture Software Re-Engineering by Prof. Jürgen Ebert.


News

22.07.07: Please participate in the evaluation of the course: www.uni-koblenz.de/~evali. If you do not have a tranaction number (TAN) yet, you can get one from Ms. Körner (room B226).
22.07.07: There are two ways for taking an exam and getting a "Schein": (a) an oral exam, (b) an assignment where a small program has to be verified. Please contact me if you would like to do either of these.
22.07.07: All the slides are now online.
09.07.07: Since room K208 is not available, the lecture on Tuesday, July 10, 10:15 is in room G409 (the lecture after that is in K208).
07.07.07: The first lecture on Tuesday, July 10 will be at 10:15 (instead of 8:30). Note, that we may have to move to a different room).
07.07.07: The slides for the first three lectures are available online now.
16.06.07: Schedule for the course is now online on the web (see below).
27.04.07: Students from the University of Koblenz should register for this lecture via the MeToo system.
08.01.07: Set up web page.


Overview

The purpose of formal methods in software engineering is to ensure, with high confidence, that systems behave according to their specification. Mostly, this is done (1) using specification languages that have a formal semantics to describe the intended behaviour and (2) using logic-based techniques to formally prove that a program satisfies its specification.

This course will give a general introduction into the basic techniques of formal specification and verification and then concentrate on the specification and deductive verification of object-oriented programs.

Participants will learn about the following topics and techniques:

We use a concrete tool to illustrate the concepts and methods that are introduced in the course: The KeY tool is an integrated tool for object-oriented design and formal verification (the book on KeY will be available to the course participants). It is developed here in Koblenz and at the University of Karlsruhe and Chalmers University, Gothenburg. The target language of KeY is a subset of Java. KeY supports UML class diagrams, formal specification in OCL, translation from OCL into logic, and an interactive theorem prover that is used to formally verify statements about specifications and programs.


Downloads

KeY System

Please download the developer version of KeY (not the official version 1.0 from the homepage) and refere to the "README" for installation instructions. Additionally you will need the 3rd Party Software. After installation run "startProver" instead of "startkey" located in the "bin" directory of your KeY installation. A tutorial on using KeY can be found here.

Exercises

Examples used for the exercises: exampleSet2.zip / exampleSet2.tar.gz


Slides


Times and Room

The course will take place in a three-week block from July 02, 2007 to July 20, 2007 in room K 208 (exception see below) at the following times:

Thu, July 5: 9.00 - 10.00 (changed!)
Thu, July 5: 12.15 - 13.45
Fri, July 6: 9.00 - 10.00
Tue, July 10: 10.15 - 11.45 Room G 409 (changed!)
Tue, July 10: 12.15 - 13.45
Thu, July 12: 8.30 - 10.00
Thu, July 12: 12.15 - 13.45
Tue, July 17: 12.15 - 13.45
Wed, July 18: 8.30 - 10.00
Wed, July 18: 12.15 - 13.45
Thu, July 19: 8.30 - 10.00
Thu, July 19: 12.15 - 13.45

There are 12 sessions of 90min. This corresponds to a regular course of 2 hours (90min) of lecture per week for an entire semester. Thus, the credit to be earned is 3.0 ECTS points.


Bernhard Beckert