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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Modelling Railway Networks with Bigraphs: Electrification, Failures, and Optimisation

  • Ricardo Almeida,
  • Susmoy Das,
  • Blair Archibald,
  • Muffy Calder,
  • Michele Sevegnani

摘要

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.