Introduction

This is the website for IA164: FMSE.

This course is given in the Faculty of Informatics (Masaryk University, Brno).
Contact person: prof. Lubos Brim.

Teacher: Rom Langerak, University of Twente, The Netherlands
e-mail: langerak@cs.utwente.nl

Additional information on the course may be found here.

Course description

This course consists of 8 parts, where each part consists of a lecture and an exercise course (both will be given in English).

  • The first 3 parts will be about the specification language Z
  • The next 4 parts will be about the process algebra FSP, and its tool LTSA
  • The last part will be about the stochastic process algebra IMC, followed by a lecture on the role of formal methods in software engineering

The assessment of this course will be in the form of a take-home examination. This examination has to be made strictly individually, and has to be handed in via e-mail (langerak@cs.utwente.nl) before Monday 24 November, 10.00 h. After the deadline the elaborations of the examination will be placed here: exercise 1 and exercise 2.

The Z part of the examination has to be made with the tool Z-EVES, which can be found on this page. Any other Z tool the student might find on the web is also acceptable. The Z tool has to be used only for type checking.

The FSP part of the examination has to be made with the LTSA tool that can be downloaded via this page.

Schedule

time place topic, slides exercises, solutions
Monday 27 Oct.
16.00-19.50		 B411 Z: Introduction
Z: Operations 		exercises 1 solutions 1
exercises 2 solutions 2
Thursday 30 Oct.
14.00-15.50		 C525 Z: Robustness exercises 3 solutions 3
Friday 31 Oct.
12.00-15.50		 C416 FSP: Introduction exercises 4 solutions 4
Tuesday 4 Nov.
8.00-13.50		 C416 FSP: Processes
FSP: Safety 		exercises 5 solutions 5
exercises 6 solutions 6
Thursday 6 Nov.
14.00-15.50		 C525 FSP: liveness exercises 7 solutions 7
Friday 7 Nov.
12.00-15.50		 C416 Stochastic Process Algebra
FM and SE 		exercises 8 (no solutions here)

Course material

Z book

The following book is out of print but freely available on the web: The Z Notation by J.M. Spivey, Prentice Hall, 1992. We advise you to read Chapter 1, and Chapter 2, sections 2.1 to 2.3.

Z-EVES tool

There is a Windows version and a Linux version. Here are some Z fonts. For running Z-EVES you need to have Python version 1.5.2 which can be downloaded from here. You need a User's Guide and maybe a Windows Manual.

FSP and LTSA

The lectures are based on the book: Concurrency: State Models and Java Programs, by Jeff Magee and Jeff Kramer, Wiley, 1999.

The LTSA software can be downloaded from here.

Here is an FSP Quick Reference Page and an overview of the FSP notation.

For exercise 5 you need the file museum.lts.

Stochastic process algebra paper

Process Algebra and Markov Chains, by Ed Brinksma and Holger Hermanns, FMPA 200, LNCS 2090, pp. 183-231, 2001.