Modelling Railway Networks with Bigraphs: Electrification, Failures, and Optimisation
摘要
Upgrading rail network infrastructure involves complex system design decisions that can be informed by suitably abstract models. Ideally, the modelling techniques support formal analysis e.g. of safety, security, resilience, and performance, the models are extensible, and they are accessible to both railway engineers and policy makers. We propose using bigraphs—a diagrammatic formal model with user-defined entities and rewrite rules—as a visual and intuitive approach to extensible railway system modelling. An example is presented: electrification rollout and the adoption of battery-powered trains that includes the impact of (probabilistic) power blackouts and supports system-level optimisation e.g. selecting which track segments to electrify, without resorting to constraint programming languages. Formal analysis via model checking is used throughout. This work represents a shift in the use of formal methods in railway engineering: from verifying isolated components such as signalling, to supporting formal, system-level design and decision-making.