T-79.300 Postgraduate Course in Theoretical Computer Science (2-10 cr)
The seminar will focuse on Modeling and Verification of Petri Nets for Systems Engineering. Applications especially from Telecommunications will also be studied (modelling of dynamical systems, e.g. mobility and protocol verification).
The use of distributed systems with asynchronous communication makes it difficult to use traditional tools like debuggers and testers because errors, even if detected, cannot be reproduced in such systems. Therefore formal models must be generated for the systems which then are analysed, for example using reachability analysis. One of the newest and most efficient reachability analyser, Maria (Modular Reachability Analyser) has been designed in our laboratory and applied to fairly large protocols (RLC in UMTS).
In this seminar, we shall investigate Modelling and Verification using High Level Petri Nets in general but also go through new publications of applications especially to Telecommunications (depending on the interests of the students attending the seminar). The main litterature is a recent book by Girault and Valk: "Petri Nets in Systems Engineering" (Springer 2003) but also conference proceedings and journal articles will be used.
Claude Girault and Rüdiger Valk: "Petri Nets in Systems Engineering", 607 p., Springer 2003. Price about 45 euro.