论文部分内容阅读
随着科学技术的不断发展,人们的生活已经慢慢步入智能信息控制化时代,背后所依赖的是各种大型高可信系统。这类系统不断地向纵深发展,系统的控制逻辑与功能实现日趋复杂,为了进一步提高系统的性能并降低维护成本,人们对系统的可靠性和安全性提出了更高的要求。因此,优化系统的体系架构与开发新的可信计算体系软件便迫在眉睫,在对系统的安全性及可靠性的性能评估便显得十分必要。而概率模型检测技术作为传统模型检测的基础上演化的一个分支,不仅能够完成自动化的验证,而且还能产生定量的结果,对系统的验证提供更为详尽的依据,对提升系统性能提供一个更加明确的方向。本文主要对高可信系统的两个实际应用场景进行研究,结合概率模型检测技术对系统进行建模验证分析。本文主要所做贡献包含如下几个方面:(1)对于传统嵌入式控制系统的构建故障模型的形式化程度不高的特点,本文结合概率模型检测技术对该系统发生故障的场景进行抽象化建模,将整个过程扩展成符合嵌入式控制系统实际场景的连续时间马尔科夫链的概率模型(Embedded Systems Continuous-Time Markov Chain,EMCTMC),对运行过程的三个阶段提出基于概率模型检测算法DCES子算法、PDES子算法以及SIES子算法描述系统运行逻辑。利用PRISM语言将系统模型和属性进行形式化描述,通过构建验证后,对系统的故障边界条件属性,不同类型的故障情况,同时还对系统的重启以及能耗进行了进一步的研究,对提升系统的稳定性以及可靠性提供了有效思路。(2)高可用性集群关键在于能提供不间断的服务,本文结合概率模型检测技术对集群的容错备援运行过程进行了建模分析。通过抽象该过程,扩展了符合集群容错备援恢复过程的连续时间马尔科夫链(Expanded Continuous-Time Markov Chain,ECTMC),提出了基于概率模型检测算法FCR子算法和REP子算法。在原模型的基础上增加了一种Producer+Queue+Comsumer队列模型策略,解决了集群系统故障与维修单元效率不匹配的问题,并对维修单元修理组件的优先级进行了定义,提升了系统的可靠性。利用概率模型检测工具PRISM对模型进行描述,使用连续随机逻辑(CSL)描述了系统服务质量(Qos)的稳定性、系统边界、故障恢复和可靠性。通过验证发现,通过增加队列模型和增加组件的优先级之后,系统的可靠性及靠灾难能力有大幅度提升,对系统改进提供了有效的解决方案。本文的研究成果在对高可信系统的可靠性验证,优化系统体系结构提供了较好的的理论指导和解决思路,扩充了概率模型检测的应用理论,为高可信系统结合概率模型检测技术的实践应用打下较好的基础。