We wish to model railway control systems in a formally precise way so that product lines can be adapted to specific customer requirements. Typically a customer is a railway operator with national conventions leading to different variation points based on a common core principle. A formal model of the core product must be precise and manipulatable so that different feature variations can be specified and verified without disrupting important properties that have already been established in the core product. Cyber-physical systems such as railway interlocking, are characterised by the combination of device behaviours resulting in an overall safe system behaviour. Hence there is a strong need for correct sequential operation with safety "interlocks" making up a process. We utilise diagrammatic modelling tools to make the core product more accessible to systems engineers. The RailGround example used to discuss these techniques is an open source model of a railway control system that has been made available by Thales Austria GmbH for research purpose, which demonstrates some fundamental modelling challenges.
展开▼
机译：我们希望以一种形式上精确的方式对铁路控制系统进行建模，以便使产品线能够适应特定的客户要求。通常，客户是具有国家惯例的铁路运营商，会根据共同的核心原则得出不同的变更点。核心产品的正式模型必须精确且可操作，以便可以指定和验证不同的功能变化，而不会破坏核心产品中已经建立的重要属性。诸如铁路联锁之类的网络物理系统的特征在于设备行为的组合，从而导致整个系统的安全行为。因此，非常需要通过安全“联锁”组成一个过程来进行正确的顺序操作。我们利用图解建模工具使系统工程师更容易使用核心产品。用于讨论这些技术的RailGround示例是Thales Austria GmbH为研究目的提供的铁路控制系统的开源模型，它演示了一些基本的建模挑战。
展开▼
