删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

轨道交通联锁领域特定语言的形式化

本站小编 Free考研考试/2022-01-02

摘要:作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题,针对联锁系统的故障随机性、行为实时性、构件可重用的特点,提出设计联锁领域特定语言IS-DSL描述具体的联锁系统的参数,并基于随机混成自动机模板自动生成联锁系统的形式化模型,以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析,根据不同案例设计其领域特定语言;其次,确定联锁系统的系统模型模板,包括环境构件模板和控制器模板,并举例抽取其随机混成自动机模板;在模板基础上定义系统模型生成过程,让领域专家可以通过领域特定语言,输入参数自动生成具体的随机混成自动机系统模型;最后以某站联锁系统为例,展示了基于模板的具体系统模型的生成过程,并通过基于系统模型的事故预测分析,证明了该方法的可行性与有效性.



Abstract:As a core subsystem of the rail transit systems, the formal modeling and analysis of the interlocking system is an important means to ensure its safety. Formalization requires both domain knowledge and formal knowledge. Since formal knowledge is difficult to master, domain experts need the help of formal experts throughout the modeling process. To solve this problem, aiming at the characteristics of fault randomness, real-time behavior, and reusability of components in railway interlocking systems, a specific language IS-DSL is proposed to describe the parameters of specific interlocking system. A formal model of interlocking system is generated automatically based on the stochastic hybrid automata (SHA) templates, to carry out further safety analysis. In this study, the model of interlocking system is analyzed firstly, and the domain specific language is designed according to different cases. Secondly, the templates of the interlocking system model, including environment component templates and controller template are established, and the SHA templates are extracted as examples. Based on these templates, the system model generation process is defined, so that the domain experts can automatically generate the specific SHA model by inputting parameters through the IS-DSL. Finally, the interlocking system of a station is taken as an example to show the generation process. The following accident prediction analysis based on this system model proves the feasibility and effectiveness of the proposed approach.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5997
相关话题/系统 知识 语言 过程 设计

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 基于堆叠泛化的设计模式检测方法
    摘要:设计模式检测是理解和维护软件系统的一项重要工作.以高效识别设计模式变体和提高设计模式识别准确率为目的,将面向对象度量与模式微结构相结合,提出一种基于堆叠泛化的设计模式检测方法.该方法应用典型的机器学习算法,分别训练度量分类器和微结构分类器,并基于两者的预测值和相关对象模型特征进一步训练,从而形 ...
    本站小编 Free考研考试 2022-01-02
  • 持久化内存文件系统的磨损攻击与防御机制
    摘要:近来出现诸多以非易失性存储器(non-volatilememory,简称NVM)作为存储设备的新型持久化内存文件系统,充分发掘NVM的低延迟和可按字节寻址等优点,优化文件访问的I/O栈和一致性机制,极大提升文件系统的性能.然而,现有持久化内存文件系统都没有考虑NVM写耐受度低的缺陷,极易导致N ...
    本站小编 Free考研考试 2022-01-02
  • 系统软件构造与验证技术专题前言
    摘要:Abstract:PDF全文下载地址:http://jos.org.cn/jos/article/pdf/5958 ...
    本站小编 Free考研考试 2022-01-02
  • 嵌入式实时操作系统内核混合代码的自动化验证框架
    摘要:“如何构造高可信的软件系统”已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出了一个自动化验证操作系统内核的框架.该验证框架包括:(1)分别对C语言程序和混合语 ...
    本站小编 Free考研考试 2022-01-02
  • 基于TEE的主动可信TPM/TCM设计与实现
    摘要:可信技术正在从被动可信度量向着下一代的主动可信监控方向发展,要求TPM/TCM模块有能力主动度量和干预主机系统,传统的TPM/TCM从架构和运行机制等方面都无法满足这种能力.TEE(trustedexecutionenvironment)技术提供了可信执行环境和主动访控能力,为构建下一代TPM ...
    本站小编 Free考研考试 2022-01-02
  • 面向推荐系统的图卷积网络
    摘要:图卷积网络是一种针对图信号的深度学习模型,由于具有强大的特征表征能力得到了广泛应用.推荐系统可视为图信号的链接预测问题,因此近年来提出了使用图卷积网络解决推荐问题的方法.推荐系统中存在用户与商品间的异质顶点交互和用户(或商品)内部的同质顶点交互,然而,现有方法中的图卷积操作要么仅在异质顶点间进 ...
    本站小编 Free考研考试 2022-01-02
  • 人工智能赋能的数据管理、分析与系统专刊前言
    摘要:大数据时代,数据规模庞大,数据管理应用场景复杂,传统数据库和数据管理技术面临很大的挑战.人工智能技术因其强大的学习、推理、规划能力,为数据库系统提供了新的发展机遇.专刊强调数据管理与人工智能的深度融合,研究人工智能赋能的数据库新技术和新型系统,包括两方面:(1)传统数据管理、数据分析技术及系统 ...
    本站小编 Free考研考试 2022-01-02
  • 轩辕:AI原生数据库系统
    摘要:大数据时代下,数据库系统主要面临3个方面的挑战:首先,基于专家经验的传统优化技术(如代价估计、连接顺序选择、参数调优)已经不能满足异构数据、海量应用和大规模用户对性能的需求,可以设计基于学习的数据库优化技术,使数据库更智能;其次,AI时代,很多数据库应用需要使用人工智能算法,如数据库中的图像搜 ...
    本站小编 Free考研考试 2022-01-02
  • 学习式数据库系统:挑战与机遇
    摘要:通用的数据库系统为不同的应用需求与数据类型提供统一的处理方式,在取得了巨大成功的同时,也暴露了一定的局限性:由于没有结合具体应用的数据分布与工作负载,系统往往难以保证性能的最优.为了解决这一问题,"学习式数据库系统"成为了目前数据库领域的研究热点,它利用机器学习技术有效捕获负载与数据的特性,从 ...
    本站小编 Free考研考试 2022-01-02
  • 一种基于元模型的访问控制策略描述语言
    摘要:为了保护云资源的安全,防止数据泄露和非授权访问,必须对云平台的资源访问实施访问控制.然而,目前主流云平台通常采用自己的安全策略语言和访问控制机制,从而造成两个问题:(1)云用户若要使用多个云平台,则需要学习不同的策略语言,分别编写安全策略;(2)云服务提供商需要自行设计符合自己平台的安全策略语 ...
    本站小编 Free考研考试 2022-01-02