面向安全攸关领域的可信技术验证应用

将可信软件的相关理论、方法与技术在航空航天、汽车电子、轨道交通等安全攸关领域开展了验证示范应用，有效地提高了安全攸关领域软件产品质量。

面向航空航天的示范应用：

1.与中国航天五院、八院合作，在航天控制系统需求分析与可信评估方面开展了技术服务;

2.该方法在重要航天型号，如嫦娥三期中得到应用，能有效检测出了需求中存在的缺陷。

根据航天嵌入式软件特性设计了可信评估和度量技术，该技术已在航天五院502所进行示范应用，并作为院标进行推广。

面向汽车电子的示范应用：

1.与普华、一汽、上汽等企业合作，针对汽车电子软件的高安全性提供汽车电子解决方案；

2.在国内，首次提出了将形式化建模与验证方法应用于自主研发的操作系统内核ORIENTAIS的开发过程；

设计了基于源代码与目标代码相结合的实时操作系统形式化验证方法。经验证过的系统通过第三方评测，获得国际认证，被批量部署在国产汽车ECU中，相关专利成功获得技术转让。

面向轨道交通的示范应用：

与上海富欣、卡斯柯等合作，采用模型驱动架构对列车控制系统中的轨旁系统提供形式化的验证方案，提高了系统的安全性与可靠性，使得系统缺陷率降低了50%。并为列车防护子系统进行了模型构造与分析，支持证明、验证和代码生成。验证后的系统通过了国际莱因最高四级安全认证。