航天多核嵌入式软件可信验证与系统原型

Embedded multicore SoC has been finding wide applications in aerospace system due to its powerful processing capability, however, the threads in a multicore concurrent program access the share variables stochastically, which makes multicore embedded software testing become more difficult than before. Taking our former research achievements as the foundation and regarding some practical requirements from the aerospace software evaluation and testing center of china, we will try to accomplish the following four aspects of research works: .1.To explore multicore embedded software modeling and verification models to prove trustworthiness of an embedded software from the standpoint of model..2.To investigate algorithms to detect atomicity violation and data race behaviors from a concurrent program with static source codes analysis and dynamic running and to probe an efficient method to quickly record and replay a program running log data to improve testing efficiency. .3.To study WCET evaluation method of an embedded concurrent software using macroscopically statistical performance analysis to forecast WCET combined with microscopically structural. .4.To research Bug characteristics for multicore concurrent program, formalization method, Bug Base organization and semantic matching algorithm based on our former C/C++ source code static analysis research achievements and to detect bugs from the concurrent program by static analysis. .At last, we will develop a system prototype to verify the above theoretical models and algorithms and apply the system to the aerospace software evaluation and testing center in practice.

嵌入式多核处理器具有较强处理能力，在航天系统得到广泛应用。多核并发程序访问共享变量时间和顺序的随机性，导致多核嵌入式软件测试困难。本项目在前期工作基础上，并考虑航天软件评测中心实际需求，拟从四个方面进行研究：1、研究基于多核的嵌入式软件建模及验证方法，从模型角度证明嵌入式软件可信性；2、针对多核程序，分别从静态代码分析和动态运行角度研究检测并发程序原子性侵犯（Atomicity Violation）以及数据竞争（Data Race）行为；为提高测试效率，研究程序执行过程记录和快速重演方法；3、由于多核Cache命中率以及并发程序运行不确定性，研究采用微观结构分析和宏观性能统计预测相结合的多核嵌入式软件WCET评估方法；4、在前期C/C++源代码静态分析基础上，研究多核并发程序BUG特征、形式化及匹配算法，检测并发程序错误。最后，开发原型系统对上述方法予以验证，并在航天软件评测中心实际应用。

嵌入式多核处理器具有较强处理能力，在航天系统得到广泛应用。多核并发程序访问共享变量时间和顺序的随机性，导致多核嵌入式软件测试困难。本项目在前期工作基础上，并考虑航天软件评测中心实际需求，从两个方面进行研究：1、研究多核嵌入式软件形式化建模及验证方法，从模型角度证明嵌入式软件可信性；2、由于体系结构特性和线程调度不确定性，研究了基于时间Petri网的多核嵌入式软件WCET评估方法，解决多核软件性能评价问题。