高可信嵌入式软件建模与验证方法的研究

In recent years, trustworthiness has become a new measurement reflecting the quality of software. Because of its special applications, compared with the ordinary software, the embedded software should be more trustworthy in terms of timeliness, reliability, security, etc. With the rising importance of information security and the enlargement of software scale, the higher demand for trustworthiness has brought great challenges into requirement analysis, design, testing and maintenance of the embedded software..This project is aimed at exploring the basic theory and method of modeling and verification of embedded software so as to lay the foundation for the design and validation. Firstly, a framework of modeling and verification for the high confidence embedded software will be proposed based on the metrics towards trustworthy embedded software. Secondly, two formal models, the structure model Z-MARTE and the behavior model ZMTA, will be presented to describe the interior constraints of high confidence embedded software. Furthermore, a novel modeling and verification method based on this formal model will be proposed and applied. Lastly, a case study in the aerospace field will be illustrated to verify the effectiveness of our methods.

近年来，软件的可信性已成为综合反映软件质量状态的新度量。与普通软件相比，嵌入式软件由于其特殊的应用领域，还具有实时性、高可靠性、高安全性等高可信性需求。面对日益严峻的信息安全和软件规模不断增大等问题，在高可信嵌入式软件的需求分析、设计、实现、测试、以及运维等各阶段均面临新的困难和挑战。本项目的研究将为解决上述问题提供理论基础，提出建模与验证的新方法。.本项目立足于高可信嵌入式软件的建模与验证基础理论和方法的研究。旨在为高可信嵌入式软件的建模与验证建立理论框架，建立可信指标体系，并提出建模与验证新方法。研究工作将半形式化与形式化方法相结合，提出高可信嵌入式软件建模与验证理论框架；提出一种可刻画高可信约束的嵌入式软件模型Z-MARTE和动态行为模型ZMTA；进一步，提出高可信嵌入式软件的建模方法和验证方法，设计相关流程，并对相应的实现技术开展研究；最后，通过航空领域中的机载软件实例开展应用研究与实验。

软件可信性已成为综合反映软件质量状态的新度量。本项目研究了面向高可信嵌入式软件可信属性的定义方法，建立了层次化的嵌入式软件可信属性指标体系，给出了各子属性的可信度量项及度量方法，可为嵌入式软件可信属性建模与验证提供依据；项目组扩展了Z语言的元模型，提出了一种可扩展的可信嵌入式软件模型 Z-MARTE，包括时间模型、结构模型、行为模型、可靠性模型、安全模型等Z-MARTE子模型，该模型能够在软件静态结构与动态行为的双重视角下，描述包括数据约束与时间约束等各类可信约束，为嵌入式软件可信属性的建模提供了一种有效途径，为软件的分析、验证与评估提供了语义基础；提出了一种基于模型检测技术的嵌入式软件可信性验证方法，提出了有限域Z-MARTE动态模型上的模型检测算法FZMCA，可用于解决嵌入式软件行为中可信约束的验证问题；提出了一种基于Z语言的嵌入式软件对象-消息-角色模型OMR，以OMR模型中的软件对象为评估单位，以对象间的通信行为规范与软件安全约束为评估依据，提出了一种嵌入式软件风险评估方法RAMES，从数据流安全的角度对嵌入式软件的安全性进行风险评估；提出了基于一致性强度的安全关键嵌入式软件的模糊评估方法，能够处理软件评估、信息安全风险评估中出现的模糊值和残缺值问题；提出了一种适用于实时嵌入式软件安全属性的形式化模型ZMsec，定义了ZMsec用例模型、静态模型和动态模型。该模型可描述嵌入式软件的时间/安全约束，增强了对嵌入式软件安全特征的表达能力。定义了时序逻辑公式ZMsecTL用于描述嵌入式软件安全属性，提出了ZMsecSD算法，将ZMsec模型转换为嵌入式软件安全状态转移图，用于模型检测和反例生成，可有效验证嵌入式软件的安全性。.项目组已发表/录用SCI期刊论文14篇，授权发明专利2项，公开发明专利6项。研究成果获得了国内外多位学者的好评。本项目的研究成果可为嵌入式可信软件的研发与评估提供技术基础，具有很好的科学意义。其研究成果在航空和船舶等可信关键领域已进行了应用研究，具有很好的应用前景。