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