随着网络技术的成熟,加速了各类网络设施、应用和服务的发展,如移动互联网、云计算等。它们渗透进了人们生活的方方面面。越来越多的设施与应用会建立在网络之上。研究如何保证它们的正确性和可靠性就变成一个有意义的课题。不同于其他软硬件系统,网络系统往往包含随机性。虽然业界目前主要采用测试来保证软硬件系统的正确性和可靠性。但是它也存在一些不足,如没有把握保证检测出系统所有的错误和其效果与测试者的经验有较大关联等。为更好地保证复杂随机系统的正确性和可靠性,我们提出了一种基于预测的贝叶斯统计模型检测方法(prediction-based Bayesian model checking)。从模型的初始状态开始,随机从模型中选择一条有限路径,并多次重复这个过程。由于有限路径是相互独立的,因此就能将所有的有限路径看作为样本,并通过贝叶斯推断(Bayesian Inference)来推断模型满足性质的概率。另外,我们利用贝叶斯统计学中先验分布与后验分布的共轭关系,在验证前预测所需样本的数量上限。并且保证一旦抽样数量达到该上限时,当前的结果已经达到了可信度与精度的要求,可立即返回。其次,根据之前所预测的上限,我们会在每次统计数据更新后,再次利用共轭关系来预测所有可能的推断结果。当所有可能的结果都与当前结果一致时,便直接返回结果。为提高对一部分复杂系统的验证效率(运行周期较长的随机系统),我们另外提出了一种启发式的抽样与验证算法。它将路径抽样与路径验证分开成两个阶段：在对路径进行验证时,尝试利用算法来定位一个“可判前缀”,而这个“可判前缀”能够直接用来判定该路径是否满足性质。而在后续的抽样中,根据之前所收集的“可判前缀”信息,便可以直接判断路径是否满足性质。从而避免耗时的路径验证。并且,它还可以与基于预测的贝叶斯统计模型检测算法相结合。SPAC(Statistical Probabilistic Approximate model Checker)是基于上述算法所实现的统计模型检测工具。通过SPAC对调度算法、分布式算法等案例进行研究后,发现在一些场景下,该算法相对于其他统计模型检测算法效率更高。并且对于运行周期较长的系统,启发式算法也可以进一步提高验证效率。
随着列控技术的快速发展以及人们出行需求的增加,城市轨道交通正在朝着高智能、高密度、高安全等目标迈进。各国研究人员积极开展新型列控系统的研发工作,其中以车载为核心的CBTC(Train-centric Communication Based Train Control,TcCB...
详细信息
随着列控技术的快速发展以及人们出行需求的增加,城市轨道交通正在朝着高智能、高密度、高安全等目标迈进。各国研究人员积极开展新型列控系统的研发工作,其中以车载为核心的CBTC(Train-centric Communication Based Train Control,TcCBTC)系统成为研究热点,其采用车车通信技术简化了控制信息的交互环节,通过对列控功能的再分配实现系统结构的优化,提升了车载的智能化程度,降低了全生命周期成本。目前TcCBTC系统正处于核心技术突破和样机研制阶段,系统运行过程中的不确定性行为可能影响行车安全。因此,系统在投入使用前必须经过严格的安全验证,以确保系统的安全高效运行。本文以随机混成自动机(Stochastic Hybrid Automata,SHA)理论作为建模基础,以统计模型检测(Statistical Model Checking,SMC)作为安全分析基础,提出了TcCBTC系统形式化建模与安全分析框架。在此基础上,通过UPPAAL-SMC对选取的实例进行分析,验证了方法的有效性,研究工作如下:(1)介绍了TcCBTC系统的国内外研究现状,深入分析了TcCBTC系统的结构、各子系统功能。建立TcCBTC系统的结构参考模型,对系统的通信接口以及各子系统通过接口交互的信息进行了分析。采用基于模型的方法结合HAZOP-I方法对系统运行过程中的风险进行辨识,即分析系统运行的不确定环境,为后续建模提供基础。(2)分析了列控系统形式化建模和验证方法的研究现状,对基于模型的安全分析方法、模型检测技术作了简要阐述。针对TcCBTC系统所处运行环境的不确定性,提出基于SHA的形式化建模方法,实现对系统运行时的混成行为和随机行为的刻画。利用DMTL语义描述所验证的性质,通过UPPAAL-SMC建立系统的形式化模型,并基于统计模型检测的思想对TcCBTC系统进行安全性分析。(3)针对TcCBTC系统运行场景进行实例研究。以移动授权场景和列车区间追踪为例,分析了各场景下系统的功能需求,确定参与此过程的子系统及其交互信息和系统运行中的不确定因素。然后,建立包含系统不确定运行环境的SHA网络模型,在静态环境中验证所建模型符合系统功能属性需求的基础上,基于SMC算法在UPPAAL-SMC中对系统模型进行定量分析。验证了不确定因素对系统的影响,并通过拟合得到对应量化指标下参数的可行域,实现对列车状态的实时监控,提高系统安全性。
信息物理融合系统(Cyber physical Systems,简称CPS)是软件和硬件设备紧密联系、相互影响相互作用的新一代智能系统。随着自动化、通信以及计算机技术的不断发展,CPS逐渐走向成熟并越来越多的应用到实际生产和生活中。人们对于CPS的要求已经不再局限于系统的功能扩展,CPS的性能指标开始被重视。在保证系统安全性和可靠性的前提下,人们倾向于采用性能更加优秀的系统。目前关于对CPS性能评价相关的形式化方法研究还很少,本次课题在对CPS特征和性能指标相关研究整理和总结的基础上,提出将形式化建模和分析的方法引入到CPS的性能评价中。利用统计模型检测和性能评价语言连续时间随机语言(Continuous Time Stochastic Language,简称CSTL)对基于HPCCS的CPS模型进行性能评价。本文的创新点如下:(1)本文在进程演算TCCS的基础上扩展概率选择和微分方程,提出一种新的信息物理融合系统建模语言HPCCS。体系结构分析与设计语言(Architecture Analysis and Design Language,简称AADL)是一种常用的体系化建模语言,利用AADL可以方便地对大型系统建模,如航电系统、列控系统等。通过扩展AADL随机行为和混成附件,提出用于CPS建模的混成AADL建模规范。由于AADL是半形式化建模语言无法直接对其进行形式化验证,本文提出AADL到HPCCS的模型转换算法,通过对转换后的HPCCS模型检测实现检测AADL模型的目的。(2)信息物理融合系统的性能评价需要一个表达能力足够并且不存二义性的性能评价语言,本文在PLTL和CTL的基础上提出一种性能评价语言CTSL。通过基于实值状态公式的CTSL可以刻画传统时序逻辑无法描述的系统性能指标。文中通过实例说明如何使用CTSL公式描述系统性能指标。(3)为了求解给定HPCCS模型的CTSL公式结果,首先利用离散化算法将模型离散化,然后通过对离散化模型的路径遍历计算出CTSL公式的精确解。由于精确求解算法随着并发进程数的增加面临状态空间爆炸的问题,本文采用贝叶斯统计模型检测算法,将CTSL分为四类公式,根据四类公式的性质分别给出贝叶斯性能评价算法。通过本文提出的贝叶斯性能评价算法,提高CTSL公式计算的效率。同时贝叶斯性能评价算法分析可以提供反例信息,供开发者找到系统的性能瓶颈。
暂无评论