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