Petri Nets is a formal modelling language for modelling distributedsystems and, in particular, notions of concurrency, non-determinism,communication and synchronisation. We have shown how Petri Netsprovide 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 thebenefits of using formal analysis methods on railway systems areshown.