Slovak, R.; Einer, S.; Tomasov, P.:
A Petri Net Based Method for Proof of Safety of Railway Operation Control System.
Integrated Design and Process Technology, Juni 2002. IDPT-2002, USA, Society for Design and Process Science.


This paper presents a formal approach to modelling system structure and behaviour based on Petri nets. It will show a functional model of the railway operation control system resulting from a system requirements specification, suitably extended in order to prove the required quality attributes according to CENELEC standards. Due to the use of a special class of stochastic Petri nets a qualitative, as well as a quantitative quality assurance of these attributes is supported. Further, with special regard to safety, the paper discusses the analysis proof methodology based on quantitative analysis, reachability investigations and their integration into the safety system design.