Abstract
This thesis is part of a larger study of the advantages of using
colored Petri nets as a modeling language for railway systems. The
railroad layout serves as a specification layer, and basic railroad
components are constructed using colored Petri nets. These basic
railroad components corresponds to physical railroad components like
turnouts, crossings, slips, etc. Then large scale colored Petri net
models of the entire subway system is generated automatically. The
colored Petri nets are then automatically translated to Maude code.
In this thesis we have expanded the algebra of the specifications, and
introduced railroad nets as an extension of colored Petri nets.
The colored Petri net components are refinable. This makes it possible
to simulate different behaviors. Several different refinements are
presented in this thesis. A tool for railroad simulation is also presented.