Techniques of Correct Software Development

Techniques of Correct Software Development

A course by Christoph Lüth, Shi Hui, Markus Roggenbach, and Lutz Schröder at the Universität Bremen 2001/2002.


Part I, WS 01/02

This is a basic course on practical approaches to correct software development.The emphasis is put on applicable techniques and effective use of tools.

Sequential as well as parallel systems will be discussed, using the algebraic specification language CASL and the process calculus CSP, respectively. On the tool side, the theorem prover Isabelle and the model checker FDR will play central roles. All methods, techniques and concepts introduced in the course will be thoroughly motivated and explained by examples and reinforced by practical exercises.

Part II, SS 02

Building on methods discussed in the preceding introductory course, substantial example applications such as, e.g., the verification of a communication protocol will be the focus of interest in this course. Students will have the opportunity to gather experience in modelling both sequential and parallel systems. To this end, the course will offer exercises concerned with the development of formal models and the investigation of their properties using tool support. The required background will be discussed in further depth in the accompanying lectures.


Chapter 1: Algebraic Specification (Markus Roggenbach)

Slides (in PDF)

Problemsheets (in ps)

Chapter 2: Theorem Proving in Isabelle (Lutz Schröder)

Slides etc.

(sometimes tarred -- untar somewhere, then acroread the pdf from same directory. Use LectXXnopause.pdf for printing. Solutions to exercises can be found in some of the tarballs under rather obvious names as .thy or .ML files. The HOL-CASL demo is part of the standard HOL-CASL-distribution) Get the old Isabelle tutorial here

Problemsheets (in ps)

Chapter 3: Process Algebra CSP - A Technique to Model Concurrent Programs (Hui Shi)

Slides (in PDF)

Problemsheets (in ps)

Examples


Chapter 4: Advanced Concepts of Algebraic Specification (Markus Roggenbach)

Problem sheet [german] (in ps)

Chapter 5: Specification Refinement in CASL (Lutz Schröder)

Slides etc.

(sometimes tarred -- untar somewhere, then acroread the pdf from same directory. Use LectXXnopause.pdf for printing.)

Lab stuff


Chapter 6: Implementing Specifications (Christoph Lüth)


Chapter 7: Process Algebra CSP -- Practice (Hui Shi)


Last modified: Mon Jun 24 12:38:22 MEST 2002