论文部分内容阅读
信息物理融合系统(Cyber Physical Systems, CPS)是一种更关注计算机与物理环境交互和协作的高级嵌入式系统,自2006年此概念被提出以来,已受到了学术界与工业界的高度关注。第一,CPS应用大都安全攸关或功耗要求严苛,在保证功能的前提下,仍必须满足一定的非功能属性,如吞吐量、能耗等,因此需要验证分析以保证其可信性;第二,CPS大都是异构的混成系统,融合了连续的物理过程和离散的系统行为,且处于高度不确定的开放环境中,因此使用传统的方法(如模型检测和定理证明)难以完成验证分析。为缓解此问题,人们开始尝试使用统计算法对系统模型的仿真Trace进行分析,求得近似结果,并给出结果的误差范围,这种方法被称为统计模型检测(Statistical Model Checking, SMC)。SMC无需遍历状态空间,但当结果精度要求较高时需要产生大量Trace(多数仿真软件的Trace生成比较耗时),性能因此大大降低,本文即针对SMC的性能问题展开深入研究。首先,对已有SMC算法的原理进行了剖析,实现了4种SMC算法,通过大量实验给出了详细的性能评估。基于实验结论,提出了一个自适应的SMC算法框架,以根据不同属性的预估概率,动态地选择合适的SMC算法。其次,为改进自适应的SMC中贝叶斯区间估计算法的不足,提出了基于抽象和学习的SMC方法,旨在减少统计分析所需的Trace数量以提高SMC的效率。其中结合已有的抽象和学习理论(如主成分分析、随机文法推断),对随机混成自动机的仿真Trace进行了概率等价抽象和简化;并基于抽象Trace学习出概率等价的系统行为模型-—前缀频率树,同时提出了树的两阶段约减算法,以有效控制树的规模,为更高效的SMC验证分析提供了良好的抽象模型。最后,介绍了我们实现的CPS建模分析平台-—Modana,基于此平台实现了本文提出的SMC改进算法,基于Modana平台建模分析了典型的CPS系统-—智能温控系统;并结合3个基准测试案例,对SMC算法改进前后的性能和准确度进行了实验性评估。结果证明,本文提出的SMC改进方法正确并且有效。