安全攸关软件系统建模与验证专题前言
摘要：随着计算机技术应用的日益普及和不断深入，软件系统的规模和复杂性急剧增大，软件在越来越多的系统中成为主要的使能部件．在航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关的应用领域，软件系统失效将导致灾难性的后果，保障软件系统的质量成为迫切的需求和挑战．建模、分析与验证是保障软件系统质量的重要环节和手段．本专题收录的14篇论文反映了近年来我国学者在安全攸关软件系统建模与验证领域的部分研究成果．《基于形式化方法的航空电子系统检测》基于形式化方法研究面向航空电子系统的检测方法，建立了航空电子系统的形式化模型，并在此基础上提出了从静态和动态两方面对航空电子系统进行检测的途径．《基于时间抽象状态机的AADL模型验证》提出了一种基于时间抽象状态机的AADL形式转换语义，并在此基础上给出了一种AADL模型的验证方法．基于形式化方法的航空电子系统检测
摘要：随着航空型号的快速发展，航空电子系统的数字化程度越来越高，软件在其中所占的比例越来越大．对航空电子系统中的软件进行测试和检测是保证航空电子系统质量及可信运行的基础．通过分析航空电子系统软件体系结构，对航空电子系统进行形式化建模，并在此基础上，提出了一种形式化的系统级综合检测方法，从静态和动态两个方面对航空电子系统进行检测，最后通过设计并实现一个综合检测系统来验证该方法的有效性．基于时间抽象状态机的AADL模型验证
摘要：提出了一种基于时间抽象状态机（timed abstract state machine，简称TASM）的AADL（architecture analysis and design language）模型验证方法．分别给出了AADL子集和TASM的抽象语法，并基于语义函数和类ML的元语言形式定义转换规则．在此基础上，基于AADL开源建模环境OSATE（open source AADL tool environment）设计并实现了AADL模型验证与分析工具AADL2TASM，并基于航天器导航、制导与控制系统（guidance，navigation and control）进行了实例性验证．基于时间STM的软件形式化建模与验证方法
摘要：状态迁移矩阵（state transition matrix，简称STM）是一种基于表结构的状态机建模方法，前端为表格形式，后端则具有严格的形式化定义，用于建模软件系统行为．但目前STM不具有时间语义，这极大地限制了该方法在实时嵌入式软件建模方面的应用．针对这一问题，提出了一种基于时间STM（timeSTM，简称TSTM）的形式化建模方法，通过为STM各单元格增加时间语义和约束，使其适用于实时软件行为刻画．此外，针对TSTM给出了一种基于界限模型检测（bounded model checking，简称BMC）技术的时间计算树逻辑（time computation tree logic，简称TCTL）模型检测方法。以验证TSTM时间及逻辑属性．最后，通过对某型号列控制软件进行TSTM建模与验证，证明了上述方法的有效性．设备驱动程序可靠性和正确性保障方法与技术研究进展
摘要：随着计算机技术的不断发展，计算机系统在安全攸关领域得到了广泛应用，其中的软件系统正逐渐成为重要的使能部件．在计算机系统中，设备驱动程序扮演了软件与硬件设备之间桥梁的角色．由于与计算机平台、操作系统、设备3个方面同时关联所导致的复杂性，设备驱动程序的开发难度大、成本高，程序中所存在的错误和缺陷常常导致系统失效，在安全攸关领域造成不可挽回的损失．以设备驱动程序可靠性和正确性保障为目标，分别从故障的隔离与恢复、正确性分析和验证、设计建模与复杂性控制这3个方面对当前相关方法和技术进行分析，为开展进一步深入的研究工作打下基础．基于数据链的软件故障定位方法
摘要：软件中存在的故障很多与数据流紧密相关，对数据流故障定位是一个具有相当难度的研究问题．通过分析变量的定义．使用关系和变量间的依赖关系，并跟踪程序运行时各种操作对变量值的影响，即，变量操作状态的变化等基本信息，提出了一种综合考虑变量操作状态变化以及变量操作状态间依赖关系的数据链模型，利用该模型对程序中数据流故障进行定位．经过实验验证，所提出的基于数据链的故障定位方法的定位结果与基于定义一使用对、基于程序切片、基于概率依赖图和基于语句覆盖这4种典型的故障定位方法进行了对比，取得了更好的定位效果．一种面向列车控制系统中安全攸关场景的测试用例自动生成方法
摘要：列车控制系统是一种安全攸关系统，为保证其安全性，要求测试过程对安全攸关场景中所有可能的运行进行完全的覆盖．现有的场景建模与测试用例自动生成方法不能完全满足这一技术需求周绕列车控制系统的安全攸关场景建模以及测试用例自动生成方法展开研究，对UML活动图扩充了事件驱动机制和时间特性描述机制，以满足对安全攸关场景建模的需要，提出了简单路径覆盖准则以定义对场景中所有运行的完全覆盖，并针对这一覆盖准则给出了自动生成测试用例的方法．以地铁列车控制系统为研究对象展开实验，表明了该方法的有效性和局限性．多处理器实时系统可调度性分析的UPPAAL模型
摘要：随着多处理器实时系统在安全性攸关系统中的广泛应用，保证这类系统的正确性成为一项重要的工作．可调度性是实时系统正确性的一项关键性质．它表示系统必须满足的一些时间要求．传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷，提出使用模型检测的方法来实现可调度性分析．提出了一个用于多处理器实时系统可调度性分析的模板，将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模，并使用uPP从L验证可调度的性质是否总被满足．符号化模型检测方法被用于推断可调度性，但是由于秒表触发的近似机制，符号化模型检测方法不能用于证明系统不可调度．作为补充，统计模型检测方法被用于估算系统不可调度的概率，并在系统不可调度时生成反例．此外，在系统可调度时，通过统计模型检测方法获取一些性能相关的信息．多分支单变量循环程序的终止性分析
摘要：对多分支单变量循环程序的终止性问题进行了研究．证明了在适定的条件下，该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点．特别地，当这类循环程序是多项式循环程序时，在给定条件下，其在实数域上的终止性问题是可判定的．面向安全攸关系统中小概率事件的统计模型检测
摘要：在开放运行环境中，安全攸关系统的不确定性行为有可能导致小概率事件的发生，而此类事件的可靠性指标往往很高，小概率事件一旦发生就会产生灾难性的后果，严重威胁到人们的生命、财产安全．因此，评估、预测小概率事件发生的概率，对于提高系统的可靠性具有重要意义．统计模型检测是一种基于模拟的模型验证技术，结合了系统的快速模拟及统计分析技术，能够有效提高模型检测的效率，适用于验证、评估安全攸关系统的可靠性，但其面临的挑战性问题之一是在可接受的样本数量下，使用统计模型检测技术难以预测、评估小概率事件发生的概率．因此，提出一种改进的统计模型检测框架，设计和开发基于机器学习的统计模型检测器，实现在相对较少的样本数量下预测和评估小概率事件发生的概率．结合轨道交通控制系统中避碰控制案例分析，进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率．面向航天嵌入式软件的形式化建模方法
摘要：航天嵌入式软件是航天型号任务成败的关键之一．航天嵌入式软件是一种周期性、多模式的软件．软件的每个模式表示系统处于一定的状态，并进行相应的复杂计算．因此，提出了一种名为SPARDL的形式化建模方法．为了满足型号应用的需求，对这一方法进行了若干改进．为了表达航天器的时序性质，提出了一种基于区间逻辑的性质规范语言.为了支持工业应用，还设计了代码生成方法．这一建模方法已在航天工业领域得到了应用．同步数据流语言高阶运算消去的可信翻译
摘要：Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言，采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度．基于这种方法，开展了从Lustre^＊（一种类Lustre语言）到C子集Clight的可信编译器的研究．由于Lustre^＊与Clight之间巨大的语言差异，整个编译过程划分为多个层次，每个层次完成特定的翻译工作．阐述了其中高阶运算消去的翻译算法，翻译过程采用辅助定理证明工具Coq实现，并进行严格的正确性证明．一种基于特征矩阵的软件脆弱性代码克隆检测方法
摘要：提出了一种基于特征矩阵的软件代码克隆检测方法．在此基础上，实现了针对多类脆弱性的检测模型．基于对脆弱代码的语法和语义特征分析，从语法分析树抽取特定的关键节点类型描述不同的脆弱性类型，将4种基本克隆类型细化拓展到更多类，通过遍历代码片段对应的语法分析树中关键节点的数量，构造对应的特征矩阵．从公开漏洞数据库中抽取部分实例作为基本知识库，通过对代码进行基于多种克隆类型的聚类计算，达到了从被测软件代码中检测脆弱代码的目的．与基于单一特征向量的检测方法相比，对脆弱性特征的描述更加精确，更具有针对性，并且弥补了形式化检测方法在脆弱性类型覆盖能力上的不足．在对android-kernel代码的测试中发现了9个脆弱性．对不同规模软件代码的测试结果表明，该方法的时间开销和被测代码规模成线性关系．一个机器检测的Micro－Dalvik虚拟机模型
摘要：给出了一个寄存器架构的虚拟机模型Micro—Dalvik，包括虚拟机指令集和虚拟机运行时状态的形式化，并以大步操作语义（big-step operational semalltics）的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换．最后，以定理的形式描述了语义满足的性质，并得到证明．这个模型的指令集包括了大部分Dalvik虚拟机指令，为获得形式语义的清晰化，它在DalvikVM指令集上进行了必要的抽象，对其实质没有改变，因而具有较大的实用性．该形式化模型通过了定理证明助手Isabelle／HOL的验证．信息物理融合系统控制软件的统计模型检验
摘要：信息物理融合系统常采用嵌入式实时多任务系统作为其控制软件，这类软件的并发和非确定性给验证带来了困难．提出了一种利用统计模型检验技术分析多任务系统的功能正确性的方法．该方法构造的时间自动机模型以模块化的方式描述了实时多任务系统中的主要成分，包括实时操作系统、周期性任务、偶发任务、共享资源以及物理环境，能够展现多任务系统的细粒度的运行过程及其对物理环境的实时响应．应用该方法分析了玉兔号月球车控制软件的一个早期版本，发现了系统运行中出现的一个特殊错误，识别了实际系统出现错误的条件，再现了出现错误的场景．基于程序频谱的动态缺陷定位方法研究
摘要：基于程序频谱的动态缺陷定位是软件自动化调试研究中的一个热点问题，通过搜集测试用例的程序频谱和执行结果，基于特定模型以定位缺陷语句在被测程序内的可能位置．对近些年来国内外学者在该研究领域取得的成果进行系统总结：首先，给出预备知识和基本假设；随后，提出缺陷定位研究框架并识别出框架内一系列可影响缺陷定位效果的内在影响因素，包括程序频谱构造方式、测试套件构成和维护、内在缺陷数量、测试用例预言设置、用户反馈和缺陷修复开销等；接着，对实证研究中采用的评测指标和评测程序进行总结和分析；然后，对缺陷定位方法在一些特定测试领域中的应用进行总结；最后，对该领域未来值得关注的研究方向进行了展望．整数漏洞研究：安全模型、检测方法和实例
摘要：C／C＋＋语言中整型的有限表示范围、不同符号或长度间的类型转换导致了整数漏洞的发生，包括整数上溢、整数下溢、符号错误和截断错误．攻击者常常间接利用整数漏洞实施诸如恶意代码执行、拒绝服务等攻击行为．综述了整数漏洞的研究进展，从缺陷发生后行为的角度提出了新的整数漏洞安全模型，总结了判定整数漏洞的充分条件．从漏洞判定规则对充分条件覆盖的角度对现有检测方法进行比较和分析．通过实例分析，讨论了整数漏洞在现实中的特征分布．最后指出了整数漏洞研究中存在的挑战和有待进一步研究的问题．一种状态事件故障树的时间特性分析方法
摘要：状态事件故障树是一种适合于描述构件化嵌入式系统失效因果链的建模技术，其顶层事件描述失效发生的结果．对顶层事件发生的平均时间进行分析，是获得系统平均失效时间参数的一种有效方法，可为系统的安全性评估提供支持．由于状态事件故障树缺乏严格语义，使得必须先对其进行形式化描述才能进行定量分析．为此，提出了一种基于交互马尔可夫链的状态事件故障树时间特性分析方法．首先前化交互马尔可夫链的交互动作，建立接互马尔可夫链模型，并基于该模型对状态事件故障树的构件和逻辑门进行形式语义描述：其次，通过并行组合构件与逻辑门的形式语义模型，得到整个状态事件故障树的形式语义模型，并在该过程中使用弱互模拟对状态空间进行约简；然后，基于状态事件故障树的形式语义给出顶层事件发生的平均时间计算方法；最后，给出飞机着陆雷达控制系统和喷淋防火系统的状态事件故障树时间特性分析的实例研究．为构件化系统失效时间特性的分析提供了一种新方法．