罗克韦尔柯林斯公司的先进技术中心副总裁约翰贝佳斯说，该公司被选的关键因素在于擅长复杂系统的安全认证和形式化方法的使用。形式化方法采用严格的数学推理和先进的分析工具，以验证系统的相关特性。公司将确保软件最初设计的正确性，这对于军用计算平台的安全性至关重要。
罗克韦尔柯林斯公司团队成员包括波音、Galois公司、澳大利亚国家信息通信技术研究机构（NICTA）、美国明尼苏达大学。
HACMS项目的目标是创建高保障赛博物理系统。这些系统必须功能正确，并满足相关的安保特性。实现这一目标需要采取截然不同的方法。因此，HACMS将采取一种基于形式化方法的清洁方法，根据可执行正式规范实现半自动化代码合成。
(工业和信息化部电子科学技术情报研究所 陈皓)
