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