题目：基于模型的嵌入式软件可信性举证技术研究

目前软件已成为计算机系统的灵魂、信息化系统的核心以及互联网应用的基石，但随着人们对功能需求不断增加，软件系统变得日趋庞大复杂和难以驾驭，缺陷和漏洞难以避免。同时由于计算实体行为存在不可控性和不确定性，软件系统越来越脆弱，很多时候不以人们期望和信任的方式工作，由此引发的事故、损失甚至灾难不胜枚举。这就是所谓的“软件可信性”问题，已引起国内外学术界和产业界普遍关注。 随着该问题凸显，近些年软件可信性相关研究风起云涌，软件可信性评估是其中一个极为重要的方向，如何确定一个软件资源是否可信以及评价可信程度是其核心的科学问题。国内外学者围绕基于完整性的可信度量方法、软件行为可信度量方法、软件可信性综合评估方法等进行了深入研究，但总体来看有效的度量方法还比较匮乏，上述方法存在着片面性、缺乏科学性和普适性等问题。相比之下，基于目标和论证的举证技术更具适用性和可行性，通过合理的论证结构和确凿的证据来证实满足了目标，在国外系统安全性领域已研究多年并在一些军用和民用标准有明确地规定。但该方法在软件可信性领域还处于探索阶段，仍存在着举证结构建模语言表达力不足、论证构建的有效性差、与软件开发过程缺乏交互等问题。 围绕这些问题，本文依据多学科多领域知识相综合、理论方法与工程实践相结合等学术思想，针对航空航天等安全关键领域的嵌入式软件，充分借鉴模型驱动架构等研究成果，研究基于模型的嵌入式软件可信性举证结构构建技术，重点解决举证元建模、举证模式等关键问题，进而形成完善的举证结构构建框架和方法，并通过案例研究来提供实践指南和范例。本文主要研究工作包括： (1)软件可信性工程基本框架研究。首先对软件可信性定义、安全关键软件概念等基础概念进行调研和探讨，接着依据工程系统论理论建立了软件可信性工程框架，从知识维、过程维、信息维和价值维四个维度对软件可信性工程的系统结构进行了阐述，为本文可信性举证技术研究尤其过程举证内容奠定了基础。 (2)基于模型的举证结构构建框架研究。首先介绍了举证结构模型、举证模式、举证模块等概念。然后提出了基于模型的举证结构构建框架MDFAS，包括元模型层、模式子层和实例子层三个层次，在利用元模型定义举证结构建模语言基础上，通过对举证模式进行实例化变换来构建举证实例结构，提供了一种通用的举证结构构建方法和途径。最后围绕举证模式实例化变换给出了嵌入式软件可信性举证结构构建过程，进而实现举证结构构建与软件过程同步交互式进行。 (3)举证结构建模语言研究。在上述构建框架MDFAS指导下，分别构建了嵌入式软件可信性举证元模型ESDCM和举证模式元模型Apattern，共同刻画了图形化的举证结构建模语言pASML，还提出了一种举证模式建模框架APMF和建模过程，最后阐述了基于OCL的pASML通用规则以及基于GSN的图示化表示法。这些举证相关元模型也为下面举证结构建模工具实现奠定基础。 (4)嵌入式软件可信性举证模式研究。在上述构建框架MDFAS和建模框架APMF指导下，利用建模语言pASML，从软件产品和软件过程两种视角构建了不同层次的嵌入式软件可信性举证模式，形成了较为完备的举证模式语言，并给出了相应实例化变换规则。该模式语言提炼和刻画出了核心论证结构和原理，是构建举证实例结构的样式和模板。 (5)举证结构建模环境实现。在上述举证元模型研究基础上，本文以Eclipse的GMF为元建模工具，在Eclipse平台上实现了举证结构建模环境，主要包括自动生成的举证结构图形化建模编辑器GSNModeler。该编辑器能够可视化地创建和编辑举证结构模型，并具有较好的操作界面和功能。 (6)案例研究。针对实际型号中两个安全关键的嵌入式软件，利用GSNModeler对上述举证模式语言中相关举证模式进行实例化变换，分别构建了较为完整的软件安全性产品举证实例和测试过程举证实例，验证了本文所提出的理论方法和工具的有效性和实用性，为举证技术的工程应用提供了实践指南和应用案例。 本文所提出的举证结构构建技术和方法，能够合理高效地构建和开发软件可信性举证结构，为软件可信性评估提供了有效可行的解决途径和手段，推动建立软件可信性工程理论体系，具有显著的理论意义。同时，通过案例研究来提供了实用的范例和指南，具有明显的工程应用价值和实践意义。