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

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

项目编号： No.91418204

项目类型： 重大研究计划

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 詹乃军

作者单位： 中国科学院软件研究所

项目金额： 170万元

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

中文关键词： 航天嵌入式软件；层次建模；一致性检测；模型转换；可信性保障

英文摘要： 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 m

英文关键词： aerospace embedded software；hierarchical modeling；consistency checking；model translation；trustworthiness guarantee