航天嵌入式软件设计一致性验证技术及其应用

In this project, we will investigate these issues including theories, methodologies, design, construction, verification of trustworthy software, related to the problem 2 defined in the NSFC Major Research Plan of Trustworthy Software. In detail, based on our previous work, we will focus on consistency checking in the design of aerospace embedded software, which is a challenging problem, also must be attacked in the undergoing NSFC project "An Integrated Environment for Trustworthy Aerospace Embedded Software and Its Demonstration and Application" in the context of the Major Research Plan. This issue is crucial and challenging in the embedded software design because: .1, Embedded softtware design is a complicated system engineering, involving hardware components, software components as well as architectures which define how a system is decomposed into component parts and how these parts interact with each other. These components and architectures should be taken into account respectively at the following four layers: circuit, logic, processor and system, which looks like a Y chart. .2,To ease a design task, the designer may develop system models at different abstraction levels. The lower-level model must be consistent with their corresponding higher-level model so that the design concerns in the higher-level model are implemented in the lower-level model. .3, Even at the same abstraction level, the designer may propose different models for different design concerns. These models must be consistent with each other so that they can be put together to form the system model. .These imply that we have to check consistency between the models for different concerns, and between the models at different abstraction levels and design layers in order to guarantee the trustworthy of the system to be developed. Consistency checking has become a challenge, as well as a hot research topic in computer science.

本研究拟针对重大研究计划中科学问题2“可信软件构造与验证”涉及的“可信软件理论、方法学、设计、构造与验证”等问题开展研究。具体说，基于我们在重大研究计划中的前期工作，针对在研集成项目《航天嵌入式软件可信性保障集成环境和示范验证与应用》中面临的航天嵌入式软件设计各阶段一致性开展研究。航天嵌入式系统设计是一个复杂的系统工程，涉及硬件、软件以及将这些构件组合起来构成系统的体系结构；同时，航天嵌入式系统的设计又需要考虑电路层、逻辑层、处理器层和系统层等，即所谓的Y图表。在同一设计层，实际设计需要设计不同抽象层次上的模型；即使在同一抽象层次，基于模型驱动设计方法需要首先对于不同关注点设计不同模型，然后这些不同关注点的模型集成为系统模型。如何保证在同一抽象层上不同关注点模型间，以及不同抽象层上设计模型间的一致性，是嵌入式系统设计中的一个难点，也是一个热点。

本课题针对重大研究计划中科学问题2“可信软件构造与验证”涉及的“可信软件理论、方法学、设计、构造与验证”等问题开展了深入研究。具体说，基于我们在重大研究计划中的前期工作，针对在研集成项目《航天嵌入式软件可信性保障集成环境和示范验证与应用》中面临的航天嵌入式软件设计各阶段一致性问题开展了研究。航天嵌入式系统设计是一个复杂的系统工程，涉及硬件、软件以及将这些构件组合起来构成系统的体系结构；同时，航天嵌入式系统的设计又需要考虑电路层、逻辑层、处理器层和系统层等不同的设计层次，而在同一设计层，实际设计需要设计不同抽象层次上的模型；即使在同一抽象层次，基于模型驱动设计方法需要首先对于不同关注点设计不同模型，然后将这些不同关注点的模型集成为系统模型。如何保证在同一抽象层上不同关注点模型间，以及不同抽象层上设计模型间的一致性，是嵌入式系统设计中的一个难点，也是一个热点。. 在本课题的资助下，我们首先完善了一套针对航天嵌入式系统的集成建模方法，并开发了相应的支撑环境，且该支撑环境中集成了各计算模型间的转换工具；其次，在上述集成建模框架中增加了协同仿真、定理证明等各阶段一致性保证技术；另外，深化了时序正确性验证技术的研究成果，提出了时序模型与代码之间的一致性验证理论和技术。本项目的理论成果获得了国际学术同行的高度关注，同时我们开发的系列工具已初步应用到了我国航天和高速铁路等安全攸关系统的设计与验证中。. 由Springer出版英文专著1部、编著1部、英文专著章节1章，在国际主流会议和杂志发表论文20篇，申请专利5项、软件著作权4项，培养博士生4人、硕士生8人，超额完成预期指标。. 通过本项目的研究，集成项目《航天嵌入式软件可信性保障集成环境和示范验证与应用》中取得的在航天嵌入式系统软件开发各阶段可信保证技术的结果集成为一个整体，从而进一步提高了航天嵌入式软件的可信性，有利于为我国航天事业做出更大贡献。