基于混成自动机的列控系统超速防护运行时监控方法
发布时间：2022-01-21 23:19
列车运行控制系统具有分布、动态、多场景融合等特点,系统缺陷在开发阶段难以完全消除。因此,需要在系统部署后实施运行时监控,在发生危险时将系统导向安全侧。运行时验证方法利用形式化语言描述系统期望满足的监控规约,并通过监控器验证系统当前的运行轨迹是否满足监控规约,从而实施运行时监控。超速防护功能的监控规约既包含复杂的混成行为又高度依赖于列车的运行环境,目前传统的运行时验证方法难以构建有效的监控规约。所以,对超速防护功能的监控规约构建方法的研究十分重要。论文主要工作包含以下四个方面:（1）提出超速防护动态监控规约构建方法。通过混成自动机建模语言建立参数化列车运行控制分层模型,计算模型关于超速防护功能顶层安全需求“列车到达行车许可终点,列车速度不大于零”的可达集。可达集中满足安全需求的部分即为超速防护监控规约。由于可达集随着列车每次运行轨迹的变化而发生改变,所以建立的超速防护监控规约具有动态性。（2）提出基于深度学习结合样条回归的分段速度监控曲线计算算法。基于该算法搭建速度监控曲线计算平台,与参数化列车运行控制分层模型实时交互,实现模型中的速度监控曲线计算功能。该方法用以提升针对不同的列车运行环...
【文章来源】：北京交通大学北京市 211工程院校 教育部直属院校
【文章页数】：103 页
【学位级别】：硕士
【部分图文】：
图２－１在线监控框架??Ｆｉｇｕｒｅ?２－１?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｎｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??
图２－２离线监控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系统的运行是作用在系统状态集合上的无穷运行轨迹。在任意时刻，系统运行轨迹都是系统无穷执行轨迹的一个有穷前缀。运行时验证方法是监控有穷前缀是否满足监控规约，给出监控结果。然而，对系统的有穷前缀的判是否同样适用于系统以该有穷前缀实际运行的无穷运行轨迹，所以需要找的有穷前缀与无穷运行轨迹的相互关系。另外，在在线监控中，发现系统危固然重要，如果监控器可以尽可能早的发现系统危险状态，保证系统安全可更为重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了预测监控器需要满足的两太性质：??公平性：给定一条有穷轨迹，如果存在不同的无穷后缀使得监控器判定出监控结果，那么该有穷轨迹应该被判定为不确定。??预测性：给定一条有穷轨迹，对于其所有的无穷后缀，监控器都将判定出监控结果，那么该有穷轨迹也将被判定为相同的监控结果。??
?Ｉ?监控结果??图２－２离线监控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系统的运行是作用在系统状态集合上的无穷运行轨迹。在任意时刻，系统当前??的运行轨迹都是系统无穷执行轨迹的一个有穷前缀。运行时验证方法是监控系统??的有穷前缀是否满足监控规约，给出监控结果。然而，对系统的有穷前缀的判定结??果是否同样适用于系统以该有穷前缀实际运行的无穷运行轨迹，所以需要找出系??统的有穷前缀与无穷运行轨迹的相互关系。另外，在在线监控中，发现系统危险状??态固然重要，如果监控器可以尽可能早的发现系统危险状态，保证系统安全可靠运??行更为重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了预测监控器需要满足的两太性质：??公平性：给定一条有穷轨迹，如果存在不同的无穷后缀使得监控器判定出不同??的监控结果，那么该有穷轨迹应该被判定为不确定。??预测性：给定一条有穷轨迹
【参考文献】：
期刊论文
[1]参数化运行时验证研究和工具实现[J]. 王哲民,陈哲,朱云龙,黄志球. 小型微型计算机系统. 2016(12)
[2]基于时间属性序列图的监控器构造方法[J]. 叶俊民,辜剑,陈曙,董威,舒绍娴. 小型微型计算机系统. 2015(07)
[3]列控设备动态监测系统的深度应用[J]. 王东. 铁道通信信号. 2014(11)
[4]一种运行时验证监控器的构造方法[J]. 张可迪,董威. 计算机光盘软件与应用. 2012(20)
[5]一种基于CPN的运行时监控服务交互行为的方法[J]. 朱俊,郭长国,吴泉源. 计算机研究与发展. 2011(12)
[6]运行时验证及其在列车运行控制系统中的应用[J]. 赵林,唐涛,徐田华,柴铭,李宪. 铁道学报. 2011(12)
[7]面向参数化LTL的预测监控器构造技术[J]. 赵常智,董威,隋平,齐治昌. 软件学报. 2010(02)
博士论文
[1]基于AOP的软件运行时验证关键技术研究[D]. 张献.国防科学技术大学 2012
硕士论文
[1]基于公式重写的实时时序约束验证及其在列控背景下的应用[D]. 李旸.北京交通大学 2015
[2]面向列控安全性监控的运行时验证方法研究[D]. 徐蛟.国防科学技术大学 2014
本文编号：3601143
【文章来源】：北京交通大学北京市 211工程院校 教育部直属院校
【文章页数】：103 页
【学位级别】：硕士
【部分图文】：
图２－１在线监控框架??Ｆｉｇｕｒｅ?２－１?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｎｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??
图２－２离线监控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系统的运行是作用在系统状态集合上的无穷运行轨迹。在任意时刻，系统运行轨迹都是系统无穷执行轨迹的一个有穷前缀。运行时验证方法是监控有穷前缀是否满足监控规约，给出监控结果。然而，对系统的有穷前缀的判是否同样适用于系统以该有穷前缀实际运行的无穷运行轨迹，所以需要找的有穷前缀与无穷运行轨迹的相互关系。另外，在在线监控中，发现系统危固然重要，如果监控器可以尽可能早的发现系统危险状态，保证系统安全可更为重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了预测监控器需要满足的两太性质：??公平性：给定一条有穷轨迹，如果存在不同的无穷后缀使得监控器判定出监控结果，那么该有穷轨迹应该被判定为不确定。??预测性：给定一条有穷轨迹，对于其所有的无穷后缀，监控器都将判定出监控结果，那么该有穷轨迹也将被判定为相同的监控结果。??
?Ｉ?监控结果??图２－２离线监控框架??Ｆｉｇｕｒｅ?２－２?Ｆｒａｍｅｗｏｒｋ?ｏｆ?ｏｆｆｌｉｎｅ?ｍｏｎｉｔｏｒｉｎｇ??系统的运行是作用在系统状态集合上的无穷运行轨迹。在任意时刻，系统当前??的运行轨迹都是系统无穷执行轨迹的一个有穷前缀。运行时验证方法是监控系统??的有穷前缀是否满足监控规约，给出监控结果。然而，对系统的有穷前缀的判定结??果是否同样适用于系统以该有穷前缀实际运行的无穷运行轨迹，所以需要找出系??统的有穷前缀与无穷运行轨迹的相互关系。另外，在在线监控中，发现系统危险状??态固然重要，如果监控器可以尽可能早的发现系统危险状态，保证系统安全可靠运??行更为重要。??Ｍａｒｔｉｎ?Ｌｅｕｃｋｅｒ等人提出了预测监控器需要满足的两太性质：??公平性：给定一条有穷轨迹，如果存在不同的无穷后缀使得监控器判定出不同??的监控结果，那么该有穷轨迹应该被判定为不确定。??预测性：给定一条有穷轨迹
【参考文献】：
期刊论文
[1]参数化运行时验证研究和工具实现[J]. 王哲民,陈哲,朱云龙,黄志球. 小型微型计算机系统. 2016(12)
[2]基于时间属性序列图的监控器构造方法[J]. 叶俊民,辜剑,陈曙,董威,舒绍娴. 小型微型计算机系统. 2015(07)
[3]列控设备动态监测系统的深度应用[J]. 王东. 铁道通信信号. 2014(11)
[4]一种运行时验证监控器的构造方法[J]. 张可迪,董威. 计算机光盘软件与应用. 2012(20)
[5]一种基于CPN的运行时监控服务交互行为的方法[J]. 朱俊,郭长国,吴泉源. 计算机研究与发展. 2011(12)
[6]运行时验证及其在列车运行控制系统中的应用[J]. 赵林,唐涛,徐田华,柴铭,李宪. 铁道学报. 2011(12)
[7]面向参数化LTL的预测监控器构造技术[J]. 赵常智,董威,隋平,齐治昌. 软件学报. 2010(02)
博士论文
[1]基于AOP的软件运行时验证关键技术研究[D]. 张献.国防科学技术大学 2012
硕士论文
[1]基于公式重写的实时时序约束验证及其在列控背景下的应用[D]. 李旸.北京交通大学 2015
[2]面向列控安全性监控的运行时验证方法研究[D]. 徐蛟.国防科学技术大学 2014
本文编号：3601143
本文链接：https://www.wllwen.com/kejilunwen/jiaotonggongchenglunwen/3601143.html
