检索结果-南通市图书馆

基于统计模型检测的Tc CBTC移动授权建模与分析

在线全文

学校读者我要写书评

暂无评论

控制工程 2023年第5期30卷 803-809,821页

作者：林俊亭闵晓琴兰州交通大学自动化与电气工程学院甘肃兰州730070

基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采... 详细信息

基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采用车车通信方式减少了控制信息的传递环节,将成为城市轨道交通领域的发展方向。移动授权(movementauthority,MA)是决定列车能否以安全间隔运行的直接因素,因此对MA生成过程进行形式化建模与分析,对避免列车碰撞具有重要意义。根据TcCBTC系统架构分析MA生成流程,确定参与功能实现的子系统,并计算出不确定性参数;通过UPPAAL-SMC建立对应的随机混成自动机网络模型;最后采用统计模型检测方法对模型进行定量分析。分析结果表明:置信度为99.95%的情况下,系统在300 ms内成功计算出MA的概率为0.9974124748,为后续TcCBTC系统开发设计提供理论参考。

关键词：随机混成自动机统计模型检测以车载为核心的列车运行控制移动授权

在线全文

学校读者我要写书评

暂无评论

基于统计模型检测的DFT定量分析方法

系统工程与电子技术 2020年第2期42卷 480-488页

作者：乔森黄志球王金永宛伟健南京航空航天大学计算机科学与技术学院江苏南京211106 南京航空航天大学高安全系统的软件开发与验证技术工业和信息化部重点实验室江苏南京211106

动态故障树(dynamic fault tree,DFT)是对系统进行安全性分析的重要手段,基于马尔可夫链的DFT求解方法存在3个难题:一是仅可分析故障概率为指数分布的系统;二是无法分析共因失效情况;三是可能导致状态空间爆炸。因此提出一种基于统计模... 详细信息

动态故障树(dynamic fault tree,DFT)是对系统进行安全性分析的重要手段,基于马尔可夫链的DFT求解方法存在3个难题:一是仅可分析故障概率为指数分布的系统;二是无法分析共因失效情况;三是可能导致状态空间爆炸。因此提出一种基于统计模型检测的DFT定量分析方法。首先将DFT分解为动态逻辑门、基本构件、共因失效关系、门门和门构件间的逻辑关系;其次将动态逻辑门、基本构件和共因失效关系基于随机混成自动机形式化规约;然后通过逻辑关系重构自动机,形成随机混成自动机网络;最后通过分析一个具有共因失效关系的服从多失效概率分布的飞机结冰探测系统,表明所提方法的有效性。

关键词：随机混成自动机统计模型检测随机系统动态故障树安全性分析

在线全文

学校读者我要写书评

暂无评论

一种面向CPS的自适应统计模型检测方法

软件学报 2017年第5期28卷 1128-1143页

作者：杜德慧昝慧姜凯强程贝教育部可信软件国际合作联合实验室(华东师范大学) 上海200062 可信软件国际联合研究中心(华东师范大学) 上海200062 上海市高可信重点实验室(华东师范大学) 上海200062

随着计算机与物理环境的交互日益密切,信息-物理融合系统(cyber-physical system,简称CPS)在健康医疗、航空电子、智能建筑等领域具有广泛的应用前景,CPS的正确性、可靠性分析已引起人们的广泛关注.统计模型检测(statistical model chec... 详细信息

随着计算机与物理环境的交互日益密切,信息-物理融合系统(cyber-physical system,简称CPS)在健康医疗、航空电子、智能建筑等领域具有广泛的应用前景,CPS的正确性、可靠性分析已引起人们的广泛关注.统计模型检测(statistical model checking,简称SMC)技术能够对CPS进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPS的效率,是目前所面临的主要困难之一.针对此问题,首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法(Bayesian interval estimate,简称BIE)在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法 AL-SMC.该方法采用主成分分析、前缀树约减等技术对仿真路径进行学习和抽象,以减少样本空间;然后,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题;最后,结合经典案例进行实验分析,实验结果表明,自适应SMC算法框架能够在一定误差范围内有效提高CPS统计模型检测的效率,为CPS的分析验证提供了一种有效的途径.

关键词：信息-物理融合系统统计模型检测抽象学习自适应性

面向安全攸关系统中小概率事件的统计模型检测

在线全文

学校读者我要写书评

暂无评论

软件学报 2015年第2期26卷 305-320页

作者：杜德慧程贝刘静上海市高可信重点实验室(华东师范大学) 上海200062

在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高... 详细信息

在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.

关键词：统计模型检测小概率事件安全攸关系统随机混成自动机机器学习

在线全文

学校读者我要写书评

暂无评论

面向复杂随机系统的启发式统计模型检测方法

计算机应用研究 2016年第10期33卷 3036-3040页

作者：何佳张敏郭延楠吕悦华东师范大学上海市高可信计算重点实验室上海200062 华东师范大学计算机科学与软件工程学院上海200062

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等,而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,提出一种启发式的统计模型检测算法。在对路径进行验证时,会查找帮助剪枝的最短前... 详细信息

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等,而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,提出一种启发式的统计模型检测算法。在对路径进行验证时,会查找帮助剪枝的最短前缀;在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少,且平均抽样路径长度更短。因此统计模型检测技术可应用于超长路径上的性质验证。

关键词：统计模型检测复杂随机系统超长路径最短前缀启发式算法 PRISM

在线全文

学校读者我要写书评

暂无评论

统计算法选择对统计模型检测效率的影响分析

计算机科学 2017年第S1期44卷 499-503,533页

作者：高婉玲洪玫杨秋辉赵鹤四川大学计算机学院成都610065

近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响。主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境。选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算... 详细信息

近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响。主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境。选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算法、智能假设检验算法及蒙特卡罗算法。采用无线局域网协议验证和哲学家就餐问题的状态可达性验证为实例进行分析,使用PLASMA模型检测工具进行验证。实验结果表明,不同的统计算法在不同的环境中对模型检测的效率有不同的影响。序贯算法适用于状态可达性性质的验证,时间性能最优;智能假设检验算法与蒙特卡罗算法适合验证复杂模型。这一结论有助于在模型检测时对统计算法的选择,从而提高模型检测的效率。

关键词：统计模型检测统计算法无线局域网协议哲学家问题 PLASMA

基于统计模型检测的无线传感器网络协议建模与分析

在线全文

学校读者我要写书评

暂无评论

基于统计模型检测的无线传感器网络协议建模与分析

作者：杨树峰郑州大学

学位级别：硕士

随着无线传感器技术的发展,无线传感器网络(Wireless Sensor Network,WSN)得到极大的关注。WSN有着广泛的应用场景,在一些危险、不易到达以及不易生存等情景下,利用无线传感器(Wireless Sensor)代替人去监测、控制目标成为自然而然的选... 详细信息

随着无线传感器技术的发展,无线传感器网络(Wireless Sensor Network,WSN)得到极大的关注。WSN有着广泛的应用场景,在一些危险、不易到达以及不易生存等情景下,利用无线传感器(Wireless Sensor)代替人去监测、控制目标成为自然而然的选择。这些传感器之间的通信就必须使用WSN,为了使无线传感器能达成监测、控制目标的目的,WSN协议必须确保功能的正确性;同时无线传感器往往资源有限、能量受限,WSN协议也要考虑性能与功耗问题。为了确保功能正确性,人们通常使用测试与仿真、定理证明以及模型检测(Model Checking)技术。测试与仿真无法对系统进行全面检测,定理证明需要过多人工干预,模型检测技术是一种可以自动对系统模型进行全面分析的检测手段,故本文使用模型检测技术进行建模分析。为了对性能与功耗进行分析,本文使用统计模型检测技术(Statistical Model Checking,SMC)。传统的模型检测技术由于状态空间爆炸问题难以对复杂系统模型进行定量分析,SMC技术利用统计学与仿真手段避免了对整个系统模型状态空间的搜索,不会遇到状态空间爆炸问题,为性能与功耗的分析提供了新方法。Minimum Cost Forward(MCF)协议是WSN网络层一种重要的协议,该协议使用了基于代价的方法形成最小代价转发路径。在此过程中无需存储路由表,数据按照最小代价路径进行传输,适用于能量与资源受限的WSN。本文针对MCF协议进行建模与分析。首先重新建立了MCF协议的时间自动机(Timed Automata, TA)模型,用时间计算树逻辑(Timed Computation Tree Logic,TCTL)语言描诉了协议的安全性、活性,在模型检测器UPPAAL上进行了验证;然后根据本文建立的TA模型,用代价时间自动机(Priced Timed Automata,PTA)对链路错误以及节点失效两种情形进行了建模,并用统计模型检测的方法分析其定量属性;除此之外,本文还利用SMC技术对协议在无损通信时的功耗进行了分析。经过分析,发现在理想情形下,MCF协议可以完成WSN的路由,但是不能均衡地消耗WSN中的能量,同时在进行有损通信时,MCF协议无法有效进行数据传输。

关键词：无线传感器网络时间自动机代价时间自动机模型检测统计模型检测

基于统计模型检测的CPS软件可信性验证研究

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于统计模型检测的CPS软件可信性验证研究

作者：陈名才苏州大学

学位级别：硕士

随着嵌入式技术、计算机技术和网络技术的不断发展，以及硬件产品性能和数据处理能力的不断提升，物联网技术得到快速发展。在此背景之下，信息-物理融合系统（Cyber-Physical Systems, CPS）作为一种新型嵌入式网络系统应运而生，并且... 详细信息

随着嵌入式技术、计算机技术和网络技术的不断发展，以及硬件产品性能和数据处理能力的不断提升，物联网技术得到快速发展。在此背景之下，信息-物理融合系统（Cyber-Physical Systems, CPS）作为一种新型嵌入式网络系统应运而生，并且引起了各国政府、学术界和工业界的高度重视。CPS是融合了计算和物理进程的复杂嵌入式网络系统，它通过嵌入式系统和网络对物理设备进行监测和控制，并通过反馈机制相互影响。CPS通常广泛用于重要基础设施的监测与控制、国防武器系统、医疗保健和智能交通等诸多安全攸关领域。由于物理环境通常具有不确定性以及物理设备本身可能出现故障，如何保证CPS的可信性成为一项重大的挑战，而CPS的可信性与CPS软件的可信性密切相关，因此保证CPS软件可信十分重要。形式化验证技术是提高软件可信性的一种重要技术，模型检测技术是软件验证时经常采用的形式化技术。传统模型检测技术的应用受到系统状态空间大小的限制，而CPS的状态空间巨大。统计模型检测是基于仿真和统计评估技术验证大型复杂系统的一种模型检测技术，可以对无限状态系统进行验证。针对传统模型检测技术难以验证CPS软件的问题，本文采用统计模型检测技术，围绕CPS软件属性验证领域所涉及的三个核心步骤：CPS软件形式化建模、CPS软件属性静态验证及CPS软件属性运行时动态验证展开研究。首先，以混成自动机为基础，通过引入通信端口得到扩展混成自动机，建立一个可以有效表达CPS软件行为的形式化模型;其次，基于统计模型检测技术，提出一种能够对CPS软件的行为属性进行静态验证的方法;最后，对CPS模型进行改进，考虑到环境因素对CPS运行结果的影响，对CPS中的不确定性等进行建模，并研究了CPS软件属性的运行时动态验证方法。使用统计模型检测技术对CPS软件属性进行验证，可以有效避免传统模型检测技术必须面对的状态空间爆炸问题，提升了CPS的健壮性和安全性。

关键词：信息-物理融合系统统计模型检测形式化验证运行时验证

基于协同仿真和统计模型检测的信息物理融合系统验证方法

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于协同仿真和统计模型检测的信息物理融合系统验证方法

作者：姜凯强华东师范大学

学位级别：硕士

信息物理融合系统(CyberPhysical System,CPS).是一种复杂的异构系统,具有异构性和不确定性等特征。因此,对该系统的仿真.、验证和分析面临着巨大的挑战。为了解决这一问题,本文提出了一种基于于协同仿真(Co-simulation)和统计模型检测(... 详细信息

信息物理融合系统(CyberPhysical System,CPS).是一种复杂的异构系统,具有异构性和不确定性等特征。因此,对该系统的仿真.、验证和分析面临着巨大的挑战。为了解决这一问题,本文提出了一种基于于协同仿真(Co-simulation)和统计模型检测(Statistical Model Checking,SMC)的验证方法,该方法能够使用SMC技术对协同仿真生成的迹进行验证和分析,为定量评估异构的CPS提供了一种有效的方法。主要包括三个阶段::首先.,使用.系统建模语言(System Modeling Language,SysML)对系统架构进行建模;其次,基于功能模拟接口(FunctionalMock-up Interface,FMI)标准构建系统的协同仿真模型并进行模型的协同仿真;最后,使用SMC技术对协同仿真得到的迹进行评估分析。本文的主要工作包括:基于时间自动机理论,验证了系统的异构组件在进行协同仿真时协同行为的正确性。首先,.提出了一种从功能模拟.单元(Functional Mock-up Unit,FMU)到时间自动机的映射规则;之后,基于时间自动机理论,将系统的仿真模型及协同仿真的主算法进行了形式化描述;最后,用UPPAAL验证工具验证了该形式化模型的有无死锁及可达性等性质。通过这种方法,验证了协同仿真过程的正确性。此外,我们还使用水箱案例展示了该方法的有效性。提出了一种基于抽象和学习的分布式SMC算法来提高SMC的效率,并给出了该算法的设计和实现。对SMC算法的效率有直接影响的因素主要有两个:验证过程中仿真器产生单条迹的速度及产生迹的数量。针对这两个因素,我们使用分布式的技术提高了产生单条仿真迹的速度,并使用抽象和学习的方法减少了验证过程中产生的仿真迹的数量,从而有效提高了 SMC的效率。最后,介绍了我们设计和开发的基于协同仿真的统计模型检测工具(Co-SMC),该工具实现了本文提出的基于FMI的协同仿真方法和改进的SMC算法。借助于该工具,我们分析了两个案例——智能温控系统和机器人路径规划系统。通过对这两个案例的验证分析,我们发现本文提出的验证分析方法是有效的,且改进的SMC算法是准确高效的。

关键词：信息物理融合系统协同仿真统计模型检测功能模拟接口分布式技术时间自动机