航天嵌入式软件可信性构造与验证的关键技术研究

本项目紧密结合航天嵌入式软件发展的实际需求，开展软件可信性需求、软件体系结构和程序的可信性构造与分析验证的基础科学问题研究，开展原型工具的研制和试验验证。本项目的研究对提高航天嵌入式软件的可信性具有重要意义。.（1）开展航天嵌入式软件可信性需求研究，开发简洁的描述可信性需求的形式化语言；.（2）研究使用随机Petri网对基于AADL语言的软件体系结构可信性构造的优化算法、使用Markov Chain对可信性的验证技术，对软件体系结构可信性特性与源程序的符合性的验证的技术研究；.（3）研究C语言的安全漏洞和航天嵌入式软件应用特点，研究并建立C语言安全规则集及检查算法；.（4）研究航天嵌入式C程序的静态分析技术，研究航天软件典型安全性质的程序标注与验证；.（5）航天嵌入式C程序的验证模型建立及验证技术研究，基于UTP理论和隔离逻辑研究C语言指针的推理技术。

本项目紧密结合航天嵌入式软件的实际需求，针对航天控制软件可信性需求建模与分析、基于AADL的航天嵌入式软件体系设计构造与验证技术和程序的可信性构造与分析验证开展了深入研究，取得的主要成果如下。.（1）针对航天控制软件的特点，提出了一套航天控制需求建模与分析框架，能够实现形式化建模、类型检查、数据流分析、仿真和验证； .（2）总结并提出了AADL分层建模方法以及描述系统中断行为的建模方法，并结合实例建立规范AADL模型；提出了包括模式变换以及行为附件在内的基于TASM的AADL转换语义定义，并对转换正确性进行了证明； .（3）针对航天嵌入式软件中突出的数据访问冲突问题，从C语言和目标码两个层次提出了中断数据竞争检测方法；针对C程序中典型数值性质，提出了高效的非凸数值抽象域；在自动测试方面，对于一类相似的性质，提出了三种学习技术提高测试数据生成时间。.项目的成果已发表论文58篇，申请专利9项，其中已授权2项，形成工具6个，大部分已经在航天型号软件研制中应用，为国家重点型号发挥了重要作用。