基于概率模型检测的高可信系统性能分析与研究

发布时间：2024-10-04 21:34

　　随着科学技术的不断发展,人们的生活已经慢慢步入智能信息控制化时代,背后所依赖的是各种大型高可信系统。这类系统不断地向纵深发展,系统的控制逻辑与功能实现日趋复杂,为了进一步提高系统的性能并降低维护成本,人们对系统的可靠性和安全性提出了更高的要求。因此,优化系统的体系架构与开发新的可信计算体系软件便迫在眉睫,在对系统的安全性及可靠性的性能评估便显得十分必要。而概率模型检测技术作为传统模型检测的基础上演化的一个分支,不仅能够完成自动化的验证,而且还能产生定量的结果,对系统的验证提供更为详尽的依据,对提升系统性能提供一个更加明确的方向。本文主要对高可信系统的两个实际应用场景进行研究,结合概率模型检测技术对系统进行建模验证分析。本文主要所做贡献包含如下几个方面:(1)对于传统嵌入式控制系统的构建故障模型的形式化程度不高的特点,本文结合概率模型检测技术对该系统发生故障的场景进行抽象化建模,将整个过程扩展成符合嵌入式控制系统实际场景的连续时间马尔科夫链的概率模型(Embedded Systems Continuous-Time Markov Chain,EMCTMC),对运行过程的三个阶段提出基于概率...

【文章页数】：67 页

【学位级别】：硕士

【部分图文】：

图3.2一天内不同故障首次发生的概率趋势图

第三章嵌入式控制系统的概率模型检测分析29顺序，为了考虑这种情况，分别单独验证各种不同故障最早发生的概率。使用CSL属性描述如下：P=?[!"down"U<=T"fail"]表示在T时间内首次发生某种故障的概率。主要讨论两种情况，分别验证在一天和一个月内两个时间段内不同故障首次发....

图3.3一个月内不同故障首次发生的概率趋势图

第三章嵌入式控制系统的概率模型检测分析29顺序，为了考虑这种情况，分别单独验证各种不同故障最早发生的概率。使用CSL属性描述如下：P=?[!"down"U<=T"fail"]表示在T时间内首次发生某种故障的概率。主要讨论两种情况，分别验证在一天和一个月内两个时间段内不同故障首次发....

图3.4每种故障导致系统最终宕机概率趋势图

第三章嵌入式控制系统的概率模型检测分析30以上都是验证在一个时间段范围内的故障发生的概率，若将时间界限去除，验证在长期时间下故障发生的概率。CSL属性描述如下：P=?[!"down"U"fail"]其中fail依次表示四种不同的故障情况，通过验证得到一个稳态的概率值，结果如表3.....

图3.5一天内不同周期数系统宕机的概率趋势图

第三章嵌入式控制系统的概率模型检测分析31终宕机的概率是随MaxCount的增大而降低。在某种程度上，增大计时器所允许的最大周期数能提高系统的容错性。但是综合考虑，传感器与输入输出处理器都是导致系统宕机的重要因素，需要选取合理的MaxCount值，使得系统宕机的可能性最校同时验证....

本文编号：4007170