Formal Modelling and Simulation of Train Control Systems Using Petri Nets

摘要: A formal model was prepared on behalf of the German railways (Deutsche Bahn AG) starting from an informal (natural language) specifications European Train Control System (ETCS) system. Proceeding existing models system design - waterfall and spiral a for developed so as to use Petri nets universal means description all phases ETCS. Following thorough detailed comparison, it decided this procedure, they permit application, different methods analysis. The method is integrated event- data-oriented approach, which shows aspects their own net levels. comprises three sub-models with environment next onboard trackside systems. This covers additional systems connected through interfaces, examples are interlocking or regulation. Starting representing context, process sub-systems modelled. Here, operations processes visualized in form scenarios, turn have access refinements specific functions. modelling supported by tool Design/CPN. It chosen after careful evaluation several tools. ETCS taken point permitting partial simulation. On basis these models, options now appear: train may expand into visualizations, algorithms can be further refined compared, used kinds tests also purposes quality assurance, go far furnishing proof safety standards. Additional development elaborated model. Our experience has shown that possible take real-life operational written natural language express content specification. demonstrated incorporate real life practices software cycles (spiral model, model) models. paper makes overview our experiences highlights various problems were encountered solved.