羅克韋爾柯林斯公司的先進技術中心副總裁約翰貝佳斯說，該公司被選的關鍵因素在于擅長復雜系統的安全認證和形式化方法的使用。形式化方法采用嚴格的數學推理和先進的分析工具，以驗證系統的相關特性。公司將確保軟件最初設計的正確性，這對于軍用計算平臺的安全性至關重要。
羅克韋爾柯林斯公司團隊成員包括波音、Galois公司、澳大利亞國家信息通信技術研究機構（NICTA）、美國明尼蘇達大學。
HACMS項目的目標是創建高保障賽博物理系統。這些系統必須功能正確，并滿足相關的安保特性。實現這一目標需要采取截然不同的方法。因此，HACMS將采取一種基于形式化方法的清潔方法，根據可執行正式規范實現半自動化代碼合成。
(工業和信息化部電子科學技術情報研究所 陳皓)
?