Latest update Feb 21, 2002
To avoid spam, all mail addresses on this page have the "@" replaced by "#".
Spring 2002
Formal Specification of Real Time Systems is a 1 cu Ph.D. level course at the Dept. of Computer Engineering (IDt), Mälardalen University. The lecturer is Martin Aronsson, SICS. Course leader at IDt is Björn Lisper, e-mail bjorn.lisper#mdh.se, phone 021-151709.
This course is based on three seminars by Martin that will be given Feb 1, Feb 8, and Feb 15, all 14-16, in the Turing Room at IDt.
There are several reasons why it is important to rigorously specify what a system should do and should not do, especially if the system is safety critical but also because of high development costs. Errors introduced early in the process are often the most expensive ones to correct, besides the fact that most of these errors are caused by misinterpretations and unnecessary. Good specifications are very important if the orderer and supplier are different companies, perhaps in different countries speaking different languages. We will in these seminars discuss a method and notation, developed and used in an industrial project, for specifying synchronous real time systems. We will also speak about how the design and implementation of the system were verified against the specification, and our experiencies from the work of going from informal requirements to validating the actual system delivered. The intention with the seminars is not to introduce another full-fledged notation and method for formal specification with a lot of nice theoretical properties, but to talk about experiences from a project where a working formalism was developed during the project.
We plan to give three seminars, with roughly the following contents:
This division is tentative, and will not necessarily be followed completely.
Here are the slides from:
All slides are in pdf format.
The text excerpt where the notation is explained (postscript format).
The examination will be through a small assignment, which is to be solved at home and handed in.
A pass on the assignment.
Presence on all three seminars.
The report on the Ariane 5 failure. (Of interest since the failure to some extent was due to a lack of proper specification of the error handling.)