T-79.193 Formal Description Techniques for Concurrent Systems (2 cr)

Spring 2004

What it is about

How to create a formal description for concurrent systems, embedded systems and real-time systems. Also methods for testing, validation and verification of such systems.

In telecommunications and multimedia applications parallel and distributed systems are used very much, but also in other fields these system are getting more and more important. There are, however, problems connected to these systems because it is very difficult to find possible errors using normal methods. Even if errors are found, the asynchronous communication may make it impossible to repeat the error.

One possible solution is to create a formal model of the system and analyse the model using reachability analysis, i.e. check every possible state of the system.

The creation of a model is not easy if it must be done manually. It is, however, much easier if there is a formal description of the system. In this case it may even be possible to generate the model automatically or, at least, using strong computer aided support.

The formal description of concurrent systems can be made in many different ways. One (almost formal) way is using the SDL (Specification and Description Language) language standardised by ITU-T and used mainly in the telecommunication sector. There are tools for translating SDL into Petri net models, analysing them and translating the results back to SDL: Emma—a TNSDL analyser and Maria—a modular reachability analyser.

This course is about formal description methods, especially SDL, but with an eye on analysis methods because it is important to create such descriptions which are easy to analyse.

Note: the course T-79.193 can be replaced by taking either the course T-79.5301 Reactive Systems or the course T-79.5302 Symbolic Model Checking.

Spring 2004: UML 2.0

Program:

START Tuesday 20 January 2004 16:30 in TB353

Seminars chaired by Docent Nisse Husberg: Tuesdays 16:30-19, room TB353 (Computer Science building).

Note: It is possible to hold the seminar talk in English or Swedish.

Course material:

• Chapters from books:
  • Laurent Doldi: UML 2 Illustrated
  • Laurent Doldi: SDL Illustrated
• Journal articles
• Research reports

In order to pass the course one has to

• attend the seminars,
• give seminar talks, and
• do the home assignment.

Newsgroup: opinnot.tieto.

Previous years: Spring 2002 Spring 2001