• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International conference on reliability, safety, and security of railway systems >A Domain-Specific Language for Generic Interlocking Models and Their Properties
【24h】

A Domain-Specific Language for Generic Interlocking Models and Their Properties

机译：通用互锁模型的领域特定语言及其属性

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

State-of-the-art railway interlocking systems typically adhere to the product line paradigm, where each individual system is obtained by instantiating a generic system with configuration data. In this paper, we present a domain-specific language, IDL, for specifying generic behavioural models and generic properties of interlocking systems. An IDL specification of a generic model consists of generic variable declarations and generic transition rules, and generic properties are generic state invariants. Generic models and generic properties can be instantiated with configuration data. This results in concrete models and concrete properties that can be used as input for a model checker to formally verify that the system model satisfies desired state invariants. The language and a configuration data instantiator based on the semantics have been implemented as components of the RobustRailS tool set for formal specification and verification of interlocking systems. They have successfully been applied to (1) define a generic model and generic safety properties for the new Danish interlocking systems and to (2) instantiate these generic artefacts for real-world stations and lines in Denmark. A novelty of this work is to provide a domain-specific language for generic models and an instantiator tool taking not only configuration data but also a generic model as input instead of using a hard-coded generator for instantiating only one fixed generic model and its properties with configuration data.
机译：最先进的铁路联锁系统通常遵循产品线范例，其中每个单独的系统都是通过实例化具有配置数据的通用系统来获得的。在本文中，我们提出了一种领域特定的语言IDL，用于指定互锁系统的通用行为模型和通用属性。通用模型的IDL规范由通用变量声明和通用转换规则组成，通用属性是通用状态不变量。通用模型和通用属性可以用配置数据实例化。这导致具体的模型和具体的属性可以用作模型检查器的输入，以正式验证系统模型满足所需的状态不变量。语言和基于语义的配置数据实例化已被实现为RobustRailS工具集的组件，用于形式化规范和互锁系统的验证。它们已成功应用于（1）为新的丹麦联锁系统定义通用模型和通用安全属性，以及（2）为丹麦的实际站点和线路实例化这些通用伪像。这项工作的新颖之处在于为通用模型和实例化工具提供了一种特定于域的语言，该实例化工具不仅将配置数据而且将通用模型作为输入，而不是使用硬编码生成器仅实例化一个固定的通用模型及其属性。配置数据。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号