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.
Teacher: Act. Professor Nisse Husberg