软件模型检测中的抽象模型研究综述

抽象是解决模型检测中状态爆炸问题的一个基本方法。对近年来软件模型检测研究中所提出的一系列抽象模型进行综述。首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分。然后根据模型的结构和功能特征,将抽象模型分为3类：1）传统的用于支持自上逼近或者自下逼近的布尔Kripke 结构;2）分别对应于3值和4值 Kripke 结构的 Kripke 模态迁移系统（Kripke modal transition systems ,KM TS）和混合迁移系统（mixed transition system ,MixTS）,可同时支持自上逼近和自下逼近的抽象;3）具有超迁移关系的广义 Kripke 模态迁移系统（generalized Kripke modal transition system ,GKM TS）和超迁移系统（hyper transition system ,HTS）,可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果。最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向。     

嵌入式机载软件安全性分析标准、方法及工具研究综述

嵌入式软件在安全关键系统中的应用,使得保障软件安全性成为软件工程领域的研究热点之一.以典型嵌入式软件系统机载软件为基础,对机载软件安全性保障的标准、方法及工具进行综述.首先,对机载软件领域所采用的软件安全性相关的标准进行简介,并给出机载软件安全性分析框架;其次,从机载软件安全性分析框架出发,将机载软件安全性保障方法划分为3个方面,即,机载软件安全需求的提取与规约、面向标准的机载软件开发、机载软件安全需求验证.对这3个方面的现有研究工作以及工业应用进行了综述;然后,针对当前适航标准的要求对机载软件安全性保证过程中软件安全证据的收集方面的研究工作进行了总结;最后,提出机载软件安全性领域存在的挑战和未来的研究方向.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

构件化嵌入式软件设计模型非功能性质验证的工具实现

嵌入式软件的非功能性质是系统高可靠性的重要构成部分.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,缺乏有效工具对系统设计的非功能性质进行分析与验证.对基于接口自动机模型的构件化嵌入式软件设计验证原型工具T-CBESD(Tool for Component-based Embedded Software Designs)进行了资源及能耗等非功能性质验证功能的扩展设计与实现,包括:资源接口自动机和能耗接口自动机模型的输入输出接口设计、UML顺序图模型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源使用性质与实时相关能量消耗特征验证算法的实现,以及一个通信构件组合系统的实例应用分析.     

集成防危性与安全性的电力CPS风险分析 研究综述

智能电网深度融合电力系统和信息系统,是一种典型的信息物理融合系统（Cyber-physical system,CPS）。针对电力CPS的网络安全攻击不仅会破坏电力系统的完整性、机密性和可用性,也可能影响电力系统的稳定运行甚至发生停电事故。集成防危性和安全性的电力CPS风险分析方法可以有效地建模和分析由于网络攻击导致电力系统失效的安全威胁场景。本文针对当前主流的集成防危性与安全性的电力CPS风险建模及分析方法进行了综述。首先针对防危性和安全性的联系与区别进行了分析,其次给出了集成防危性与安全性的电力CPS建模及分析框架。根据该框架,从电力CPS风险建模、定性分析、定量分析三个方面对现有的研究工作进行了综述。最后对现有的研究工作中的问题进行了总结并给出了未来的研究方向。本文可以为电力CPS的风险建模与分析提供参考。     

基于BPEL和ws-Tx的Web服务组合事务协调框架研究

针对当前Web服务事务协调框架中缺乏对服务组合流程定义的支持而需要在协调过程中手动定义业务流程的问题,提出了一种支持流程和事务语义自动抽取的服务组合事务协调框架。该框架从扩展了事务语义的业务流程执行语言(Business Process Execution Language,BPEL)中抽取协调信息,并结合Web服务事务规范(Web Services Transaction,WS-TX)所定义的协调器实现了服务组合的全局事务协调。通过将WS-TX在事务协调和BPEL在业务流程设计方面的优势相结合,该框架将业务逻辑与事务处理逻辑有效地分离。最后通过实例分析说明了该框架的可行性。     

机载软件适航认证标准新进展及展望

为了满足机载软件适航认证的迫切需求,对机载软件适航认证标准进行分析研究.阐述了DO-178B的发展动因及过程,总结了随着软件开发技术的快速更新DO-178B所表现的不足.说明了对DO-178B进行更新的必要性,并将即将发布的新版本DO-178C与DO-178B进行了对比.根据对比结果重点分析了DO-178C的4个新增特性.对DO-178C所带来的影响以及未来应用进行了展望.     

T-CBESD:一个构件化嵌入式软件设计模型验证工具

现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.     

循环对称化简及在三值模型上的扩展

为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型——三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.