软件学报安全攸关软件系统建模与验证专题PPT.pptx

软件学报安全攸关软件系统建模与验证专题;;1《基于形式化方法的航空电子系统检测》;《基于形式化方法的航空电子系统检测》;《基于形式化方法的航空电子系统检测》;《基于时间抽象状态机的AADL模型验证》;3《基于时间STM的软件形式化建模与验证方法》;3《基于时间STM的软件形式化建模与验证方法》;4《设备驱动程序可靠性和正确性保障方法与技术研究进展》;5《基于数据链的软件故障定位方法》;6《一种面向列车控制系统中安全攸关场景的测试用例自动生成方法》;7《多处理器实时系统可调度分析的UPPAAL模型》;8《多分支单变量循环程序的终止性分析》;9《面向安全攸关系统中小概率事件的统计模型检测》;模块1学习型模型检测器 输入：系统模型a+有界线性时态逻辑公式 输出：用‘经典模型检测算法’判断‘单个样本trace’是否满足‘属性约束’，得到统计分析样本 Trace分割与特征提取 目的：找到一个合适的时间点,使其前段 Trace 在尽可能短的条件下最大程度地包含对预测有用的信息,以便 SVM 预测后段 Trace 的信息. 思想：条件概率。假设在 A 事件发生的情况下,B 事件更有可能发生,如果 P(A)P(B),则先在模拟Trace 的过程中找到 A 事件的发生点,在此前提下向后进行多次模拟,以提高捕获到 B 事件的可能性. 基于属性约束和随机行为的特征提取方法：1.确定需要提取的特征变量;2.根据特征变量提取训练集中 Trace 的具体特征.;SVM:机器学习模型，用于预测生成新的样本。如果样本可信，则使用预测结果，并开始下一次模拟；不可信，则进入后段仿真器，模拟出完整的Trace，检测其结果。;10《面向航天嵌入式软件的形式化建模方法》;个人： SPARDL数用于描述需求的2层语言，上层是模式图，下层是对应的形式化描述。;概率模型检测 概率模型检查把性质 p 在模型的一次执行(一条路径)上是否成立视为一个服从两项分布的随机变量.概率模型检查主要考虑以下两个问题:给定模型 M 和性质 p,1) 估算在模型 M 的任意一条路径 t 上,p 成立的可能性,即参数估计;2) 判断上述可能性是否大于给定的阈值,即假设检验.;11《同步数据流语言高价运算消去的??信翻译》;12《一种基于特征矩阵的软件脆弱性代码克隆检测方法》;;13《一个及其检测的Micro-Dalvik虚拟机模型》;14《信息物理融合系统控制软件的统计模型检验》;统计模型检验： 将模型检验和统计方法相结合，利用可执行模型的多次相互独立的模拟，估计系统满足某性质的概率。 优点：所需资源与系统描述呈大致线性关系，因而避免了状态爆炸问题，且能够解决不可判定问题。 本文贡献： 系统分解为实时OS、应用任务、物理环境，分别建模，然后用‘同步通道’刻画各部分的交互（没有见到同步通道描述的交互）。 时态逻辑描述被验证的性质（没有见到）。;总结-1;总结-2