Sammendrag
Petri Nets is a formal modelling language for modelling distributed
systems and, in particular, notions of concurrency, non-determinism,
communication and synchronisation. We have shown how Petri Nets
provide a good framework for modelling railway systems, which are large and complex concurrent systems. The thesis consists of three main parts:
- Using Petri Nets to model railway systems with a component based
approach, mostly focusing on the trackwork of the systems.
- Defining an algebraic technique for specifying and automatically
constructing large scale Petri Nets, in the domain of railway
systems.
- Implementing a tool using this technique.
In the thesis, Oslo subway is modelled using Petri Nets and the
benefits of using formal analysis methods on railway systems are
shown.