基于模型的嵌入式软件测试与验证技术及针对国产列车控制系统的实例研究

高可信嵌入式软件系统都具有安全攸关特性，一旦失效可能导致灾难性的后果，因而其测试和验证是重要研究课题。本项目申请针对高可信嵌入式系统的高复杂度、大规模、强实时、高安全、高可靠等要求，基于测试和验证目的，研究扩展UML、AADL、混成自动机以完成对嵌入式系统预期行为和控制逻辑的建模方法，研究基于模型的嵌入式系统的测试和验证方法，并用符号执行与约束求解、随机方法、反馈方法、机器学习方法、路径遍历等方法改进和优化基于模型的测试生成方法与验证方法。列车控制系统是典型的高可信嵌入式系统，其可信性要求与民航、核电、金融等系统同为最高类别，本项目选择在研的国产CJ-7型CBTC列车控制系统作为实例，探索嵌入式系统的建模、基于模型的测试和验证技术在工程实践项目中的适用性问题，为基于模型的测试与验证方法在高可信嵌入式系统的可信保障提供示范应用。