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

软件学报安全攸关软件系统建模与验证专题文章整体分类1《基于形式化方法的航空电子系统检测》方法：模型检测质量：一致性——系统结构设计的资源是否满足需求中性能指标的配置要求，即：系统结构对应的资源能否满足配置（静态检测）；可用性——系统的执行环境是否能保证系统任务的正常执行（动态检测）。模型：系统结构、资源、任务的形式化建模检测标准：一致性——a.配置文件一致性：软件配置项是否满足需求（不同级别配置文件是否一致）；b.系统环境状态适配性（环境即资源，当前状态能否满足性能指标）。可用性——生成的“检测用例”。实例：航空电子系统仿真平台《基于形式化方法的航空电子系统检测》航空电子系统静态建模API：输入/输出+约束；性能指标PI：资源属性名+数量；配置文件CONF：文件属性+属性值；软件配置项CSCI：1+2+3；分系统SS：1+2+3+4；航空电子系统ES：1+2+3+5.功能建模组件关系建模《基于形式化方法的航空电子系统检测》动态建模：窗口树、任务执行过程状态图《基于形式化方法的航空电子系统检测》检测过程2《基于时间抽象状态机的AADL模型验证》方法：模型检测实际工作：AADL（系统体系结构设计与分析语言）

TASM（时间抽象状态机）质量：依赖于TASMToolset和UPPAAL模型：AADL图形化模型检测标准：任务的参数描述（表格）实例：导航、制导与控制系统GNC的AOCS子系统（控制计算机/姿势与轨道控制系统）工具：AADL2TASM《基于时间抽象状态机的AADL模型验证》思路：1.分别对AADL和TASM语法进行抽象，然后给出映射关系，并基于ML的元语言形式定义2者的转换语义规则；2.系统AADL建模AADL2TASMTASMToolSet分析完整性、一致性、时间行为和资源行为仿真UPPAAL检测死锁、安全性、活性、实时性。3《基于时间STM的软件形式化建模与验证方法》方法：模型检测质量：可信性（时间和逻辑属性）模型：TSTM——给STM加了‘时间和语义约束’（STM——状态迁移矩阵，一种基于表结构的状态机建模方法，前端为表格形式，后端是严格的形式化定义）检测标准：用‘时序逻辑语言’TCLT定义的所需满足的性质。实例：列车控制系统3《基于时间STM的软件形式化建模与验证方法》本文方法：软件TSTM建模，刻画软件的行为特征；属性的TCTL描述检测方法：基于界限模型检测（BMC）技术的‘时间计算树逻辑（TCTL）’模型检测方法——模型和待验证属性的否定形式进行合取，构建BMC公式，BMC公式的求解问题归约为逻辑公式的可满足性判定，即：SAT/SMT实例。4《设备驱动程序可靠性和正确性保障方法与技术研究进展》综述性论文质量：驱动程序的可靠性和正确性。程序故障隔离与恢复、正确性分析和验证、设计建模与复杂性控制。5《基于数据链的软件故障定位方法》方法：代码分析质量：程序的数据流相关的逻辑故障定位（程序设计逻辑故障，定位到方法内的代码）模型：数据链——每个变量上的‘定义操作状态轨迹’及其之间的依赖关系。分析对象：程序代码检测方法：先用现有方法将逻辑故障定位到方法；再用本文方法中方法内定为——变量故障疑似度分析：a.对故障疑似方法建立‘数据链’；b.用a的数据链构建概率数据链模型。c.疑似度排序实验对比6《一种面向列车控制系统中安全攸关场景的测试用例自动生成方法》本文工作：扩展了活动图，加入了a.事件驱动机制；b.时间约束.覆盖准则：a.循环只执行一次；b.不同的并发分支并发执行（同时向前执行一步）；c.所有‘简单路径’被覆盖（从a、b两条准则得到的活动图执行路径）。本文测试用例生成方法：扩展活动图建模，并找出其中的‘简单路径’；明确‘被测系统’的边界；执行简单路径，并沿路收集外部环境向被测系统发送的事件，作为‘测试输入’，被测系统向外部环境的输出作为‘结果序列’。测试用例=环境传给被测系统的信息（特定时间）+被测系统的观察结果+时间上需满足的约束。实例：地铁列车控制系统7《多处理器实时系统可调度分析的UPPAAL模型》方法:模型检测（偏硬件，主要数UPPAAL的使用）质量：可调度性——系统必须满足的时间要求。模型：UPPAAL模型性质：时间自动机建模可调度性相关的模块（实时任务、运行平台、调度管理）检测：UPPAAL检测实验：对象——智能手机GSM系统的21个任务本文贡献：给出了多处理器实时系统可调度分析的模板8《多分支单变量循环程序的终止性分析》方法：代码分析质量：带多个分支的单变量循环程序的终止性问题（系统中有无死循环，是正确性的基础）（可信计算）主要结果：称由迭代函数F和循环条件形成的区域I所构成的循环程序P(F,I)在实数域\是不可终止的,如果存在一点x0∈\,使得{()}FxIi00i+∞=⊆.这里,Fi=FDFD…DF表示函数的复合.如果那样的x0不存在,则称循环P(F,I)在实数域上可终止.定理1.令f:R6R为一维连续映射.I为一闭区间.循环程序

P1Whilex∈Ido

{x:=f(x)}

是不可终止的充分必要条件为迭代映射f在闭区间I上有不动点.……实例应用：对多分支单变量多项式循环程序，可通过实代数工具验证定理中条件是否成立；判定不动点是否落入到循环条件形成的区域问题，可转为半代数系统，通过实代数工具求解。

9《面向安全攸关系统中小概率事件的统计模型检测》方法：基于机器学习的统计模型检测算法统计模型检测SMC——评估系统模型满足属性约束的概率区间机器学习（用于生成更多样本）质量：可靠性（在相对较少的样本数量下，预测、评估小概率事件的发生概率）本文框架：输入：a.目标系统的可执行模型（随机混成自动机模型SHA）；b.属性约束的‘概率有界线性时态逻辑（PBLTL公式）’；c.统计精度参数。输出：在有限的资源约束下，系统模型a满足属性约束b的概率区间。2个模块：学习型模型检测器+自适应统计分析器实例：基于通信的列车控制系统<模块1>学习型模型检测器输入：系统模型a+有界线性时态逻辑公式输出：用‘经典模型检测算法’判断‘单个样本trace’是否满足‘属性约束’，得到统计分析样本Trace分割与特征提取目的：找到一个合适的时间点,使其前段Trace在尽可能短的条件下最大程度地包含对预测有用的信息,以便SVM预测后段Trace的信息.思想：条件概率。假设在A事件发生的情况下,B事件更有可能发生,如果P(A)>P(B),则先在模拟Trace的过程中找到A事件的发生点,在此前提下向后进行多次模拟,以提高捕获到B事件的可能性.基于属性约束和随机行为的特征提取方法：1.确定需要提取的特征变量;2.根据特征变量提取训练集中Trace的具体特征.

SVM:机器学习模型，用于预测生成新的样本。如果样本可信，则使用预测结果，并开始下一次模拟；不可信，则进入后段仿真器，模拟出完整的Trace，检测其结果。<模块2>自适应统计分析器将<模块1>的结果作为统计分析样本，执行统计模型检测，判定现有样本是否满足精度要求，满足这结束，否则返回<模块1>生成更多样本trace.SPRT顺序概率比检验；BHT贝叶斯假设检验；BIET贝叶斯区间估计检验。10《面向航天嵌入式软件的形式化建模方法》研究对象：周期性控制系统的需求获取、表示、分析验证方法：模型检测（分析所建的需求模型）本文思路：航天需求描述语言SPARDL形式化建模方法——用一系列‘模式’来体现嵌入式控制系统的‘行为特征’，每个模式可以周期性地执行一系列过程。核心是模式图，描述模式和模式间的变迁。时序性表示——给出了ITL（基于区间逻辑的性质规范语言）性质模板。从SPARDL自动生成C代码（给了原理），并快速仿真。实例：某深空探测信号软件，用于钻探取土（没有给出任何数据）个人：SPARDL数用于描述需求的2层语言，上层是模式图，下层是对应的形式化描述。概率模型检测概率模型检查把性质p在模型的一次执行(一条路径)上是否成立视为一个服从两项分布的随机变量.概率模型检查主要考虑以下两个问题:给定模型M和性质p,

1)估算在模型M的任意一条路径t上,p成立的可能性,即参数估计;

2)判断上述可能性是否大于给定的阈值,即假设检验.

11《同步数据流语言高价运算消去的可信翻译》两种语言差距较大：Luster*有时钟同步、数据流、并发及数据流对象，其‘变量’和‘表达式’都表示一个‘流数据（给定类型的值序列+一个时钟）’；Clight有顺序控制流特征。高阶运算：一个对数组或输入参数列表进行循环计算的过程。12《一种基于特征矩阵的软件脆弱性代码克隆检测方法》方法：代码检测质量：脆弱性（如缓冲区溢出、内存多次释放、指针误用等）本文思想：建立一个已发现的脆弱性代码数据库,从代码的相似度层面进行检测,查找某个软件系统出现的脆弱性代码在其他软件中的分布情况,就可以检测出更多的脆弱点.提出多类脆弱性检测模型模型CVdetector实验数据对比10维向量(stmtexp,decl,incr,cond,assign,mul,add,fun_call,fname,fpara)

13《一个及其检测的Micro-Dalvik虚拟机模型》形式化虚拟机模型，对指令集和运行时状态进行了形式化，然后推理证明该虚拟机的正确性。14《信息物理融合系统控制软件的统计模型检验》方法：模型检测质量：系统功能的正确性本文内容：基于时间自动机，模块化描述实时多任务系统，然后提出一种利用统计模型检验技术，分析系统功能正确性。模型：调度器、周期性任务、偶发任务、的时间自动机模型。检测标准：人工分析出