检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

基于形式化方法的平交道口控制系统安全设计

西南交通大学学报 2023年第1期58卷 109-116页

作者：王霞王恪铭徐扬唐伟健西南交通大学计算机与人工智能学院四川成都610031 西南交通大学系统可信性验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都610031 西南交通大学信息科学与技术学院四川成都610031

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限... 详细信息

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.

关键词：平交道口控制系统需求规范安全苛求系统形式化方法

基于UPPAAL的智能网联道口控制系统建模与验证

在线全文

学校读者我要写书评

暂无评论

计算机仿真 2024年

作者：刘昱含王恪铭西南交通大学计算机与人工智能学院西南交通大学信息科学与技术学院西南交通大学系统可信性自动验证国家地方联合实验室

铁路平交道口作为铁路与道路运输交汇的重要地段，一旦发生事故会造成极大的人员伤亡与财产损失。现有的道口系统大多存在设备不完善、自动化与智能化建设程度较低以及缺乏可靠的安全规范等问题。为了顺应当前智能化交通的发展需求，针... 详细信息

铁路平交道口作为铁路与道路运输交汇的重要地段，一旦发生事故会造成极大的人员伤亡与财产损失。现有的道口系统大多存在设备不完善、自动化与智能化建设程度较低以及缺乏可靠的安全规范等问题。为了顺应当前智能化交通的发展需求，针对上述问题，提出了一种智能网联道口安全防护控制系统。通过分析系统的功能流程，建立系统的信息交互网络，明确系统的功能安全需求。基于UPPAAL对系统进行建模仿真与验证，结果表明性质验证均通过，满足系统的充分性、一致性、实时性与安全性需求，最后对验证后的系统进行嵌入式开发与实现，为未来道口系统的设计及其安全规范提供了理论参考。

关键词：平交道口系统设计自动机理论形式化方法模型验证

车站联锁系统行为验证与数据确认的形式化方法

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

西南交通大学学报 2021年第3期56卷 587-593,610页

作者：王恪铭王霞程鹏刘宁张传东西南交通大学信息科学与技术学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都610031 西南交通大学唐山研究生院河北唐山063000 北京和利时系统工程有限公司北京100176

车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速... 详细信息

车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验证过程,结合给定场景联锁数据的有效性确认,发现并纠正系统需求及分析过程中造成的潜在行为缺陷;通过功能仿真与验收测试,进一步确认了通用模型与联锁数据的正确性.结果表明:本文方法提高了基于模型开发过程的准确性与层次性,验证了系统通用行为状态,且结合公理验证,实现了联锁数据的确认,并能基于模型进行功能场景仿真与测试,从而可进一步提高系统通用功能原型的可靠性.

关键词：车站联锁系统形式化验证定理证明数据确认功能仿真测试

基于网络连接及服务中心选择的高铁路网区域划分方法

在线全文

学校读者我要写书评

暂无评论

中国铁道科学 2018年第4期39卷 123-130页

作者：张强锋王恪铭倪少权吕红霞西南交通大学交通运输与物流学院四川成都610031 西南交通大学信息科学与技术学院四川峨眉山614202

高速铁路路网的区域划分对于区域性运行图的编制具有重要意义。结合路网的邻接特性,并考虑动车储备与检修能力进行区域中心的选择,以区域内的最小连接距离、最大平均连接紧密度为目标,建立高铁路网区域划分混合整数规划模型,并设计向量... 详细信息

高速铁路路网的区域划分对于区域性运行图的编制具有重要意义。结合路网的邻接特性,并考虑动车储备与检修能力进行区域中心的选择,以区域内的最小连接距离、最大平均连接紧密度为目标,建立高铁路网区域划分混合整数规划模型,并设计向量编码方式的遗传优化求解算法、高铁客运周转量折算方法。最后,以中国铁路总公司所属路网区域构建算例,对比聚类算法说明文中模型与算法的有效性与适应性,分析目标函数权重系数、最大服务半径与最大服务容量约束对划分结果的影响,得出服务半径系数、服务容量系数的设定方法。

关键词：高铁路网区域划分路网连接中心选择向量编码遗传算法服务半径服务容量

在线全文

学校读者我要写书评

暂无评论

基于近期文字极性分配的学习子句评估算法

计算机工程与科学 2023年第11期45卷 1941-1948页

作者：冯心妍吴贯锋张丁荣王恪铭西南交通大学信息科学与技术学院四川成都611756 西南交通大学系统可信性自动验证国家地方联合工程实验室四川成都611756 西南交通大学数学学院四川成都611756 西南交通大学计算机与人工智能学院四川成都611756

为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句... 详细信息

为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句有用性的方法,从而保留对求解最有促进作用的学习子句,以提高求解效能。从捕获学习子句近期的极性分配出发,结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省,来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准,针对其在子句评估环节的算法进行改进测试。实验结果表明,这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率,有效改善了原有求解器在一些问题上求解耗时过长的问题,并在先进求解器的水平上多求解了2个合取范式CNF文件,单个文件的平均求解时间缩短了13~34 s。

关键词： SAT问题子句评估策略 CDCL 学习子句

项目沉浸式教学在高校人工智能课程中应用的改革与探索

在线全文

学校读者我要写书评

暂无评论

中国多媒体与网络教学学报(上旬刊) 2023年第12期 53-56页

作者：李可杜圣东郭东明王恪铭杨燕西南交通大学计算机与人工智能学院

人工智能这一战略性技术正驱动着新一轮科技革命与产业变革，人工智能人才的培养尤其重要。高校人才培养不仅要求学生掌握本业知识，还要具备一系列软硬能力，如国际视野、沟通能力、科学思维和创新能力。基于此，本文以项目沉浸式教学... 详细信息

人工智能这一战略性技术正驱动着新一轮科技革命与产业变革，人工智能人才的培养尤其重要。高校人才培养不仅要求学生掌握本业知识，还要具备一系列软硬能力，如国际视野、沟通能力、科学思维和创新能力。基于此，本文以项目沉浸式教学理论为基础，对大学人工智能课程进行改革和探讨，旨在培养具有国际视野、科学思维和解决实际复杂问题的创新型人工智能人才。本文分析了项目沉浸式教学应用于人工智能课程的可行性，并从教学模式、教学内容和教学活动管理三个方面阐述了该课程的实施步骤。

关键词：项目沉浸式教学人工智能课程改革

基于知识图谱和故障树的高速铁路事故致因分析

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

铁路计算机应用 2023年第7期32卷 14-18页

作者：张丁荣王恪铭冯心妍西南交通大学信息科学与技术学院成都610031 西南交通大学计算机与人工智能学院成都610031 西南交通大学系统可信性自动验证国家地方联合工程实验室成都610031

针对高速铁路(简称:高铁)事故开放共享程度不高,数据条块化、垂直化,信息碎片化等问题,基于知识图谱构建高铁事故的本体层及数据层,实现事故数据的资源整合,使用图数据库表达事故致因逻辑关系,通过Python编程生成高铁事故致因故障树,完... 详细信息

针对高速铁路(简称:高铁)事故开放共享程度不高,数据条块化、垂直化,信息碎片化等问题,基于知识图谱构建高铁事故的本体层及数据层,实现事故数据的资源整合,使用图数据库表达事故致因逻辑关系,通过Python编程生成高铁事故致因故障树,完成对高铁事故的致因分析。分析结果表明,人为因素中的“违规作业”“监管不力”及环境因素中的“恶劣天气”导致了更多高铁事故的发生。据此结果,为铁路相关部门防范重大事故发生提出了切实可行的建议。

关键词：高速铁路事故致因知识图谱故障树事故分析

在线全文

学校读者我要写书评

暂无评论

灾后重建地区新增血站的选址问题研究

运筹与管理 2012年第1期21卷 136-141页

作者：王恪铭马祖军郑斌西南交通大学交通运输与物流学院四川成都610031 2.西南交通大学经济管理学院四川成都610031

根据灾后重建地区血液保障体系建设的实际情况,考虑血站间的依附系数对血站布局的影响,建立了一种p-中值模型用来解决新增血站的选址问题,并设计了一种遗传-禁忌混合算法对模型进行求解.之后以汶川大地震灾区——四川省阿坝州为例进行... 详细信息

根据灾后重建地区血液保障体系建设的实际情况,考虑血站间的依附系数对血站布局的影响,建立了一种p-中值模型用来解决新增血站的选址问题,并设计了一种遗传-禁忌混合算法对模型进行求解.之后以汶川大地震灾区——四川省阿坝州为例进行了实例分析,得到了不同p值与依附系数下的新增血站选址方案,以期为相关部门规划灾后重建地区的血液保障体系提供理论依据与决策参考.

关键词：灾后重建设施选址问题血站依附系数遗传—禁忌混合算法

来源：博看期刊评论

在线全文

博看期刊

学校读者我要写书评

暂无评论

道口管理系统多参数的形式化建模与验证

综合运输 2019年第2期41卷 65-72页

作者：王霞刘宁王恪铭西南交通大学交通运输与物流学院四川成都610031 西南交通大学唐山研究生院河北唐山063000 西南交通大学信息科学与技术学院四川成都610031

铁路平交道口作为铁路安全的瓶颈,其作业流程的缺陷是导致安全事故发生的重要原因之一。而现有道口管理规范大部分只针对单线接车,对于双线双向接车没有给出详细的规范。为了丰富实际流程,基于道口管理规范,探讨双线双向道口连续接车的... 详细信息

铁路平交道口作为铁路安全的瓶颈,其作业流程的缺陷是导致安全事故发生的重要原因之一。而现有道口管理规范大部分只针对单线接车,对于双线双向接车没有给出详细的规范。为了丰富实际流程,基于道口管理规范,探讨双线双向道口连续接车的问题,同时考虑道口接车作业流程中存在的异常,提出流程方案。分析系统环境属性、功能属性和安全属性,并利用UPPAAL时间自动机进行建模仿真,对模型的属性进行验证,根据验证结果确认方案流程的可行性。结果表明,本文所提出的多参数道口作业流程更符合实际情况,改进了多列车接车流程,并提出了接车过程中异常情况下的应对方案。

关键词：平交道口双线双向多参数安全模型验证