為方便軟考考生對(duì)軟件評(píng)測(cè)師考試知識(shí)點(diǎn)的檢測(cè)，希賽軟考頻道為考生帶來(lái)軟考軟件評(píng)測(cè)師考試知識(shí)點(diǎn)填空檢測(cè)的內(nèi)容（完整版可在本文文首本文資料處或文末的資料下載欄目下載）。

軟考軟件評(píng)測(cè)師考試知識(shí)點(diǎn)填空檢測(cè)（28）內(nèi)容如下：

第28章 可信軟件驗(yàn)證技術(shù)

可信軟件的驗(yàn)證技術(shù)

·形式化建模與方法

形式化驗(yàn)證技術(shù)：定理證明、________。

·可信軟件驗(yàn)證工具

________是一款開(kāi)源的形式化軟件驗(yàn)證工具，用來(lái)分析和驗(yàn)證并發(fā)系統(tǒng)邏輯是否一致的輔助驗(yàn)證器，它主要是針對(duì)軟件檢測(cè)，而不是驗(yàn)證硬件是否能高效運(yùn)行。

________。

________是由ClearSy開(kāi)發(fā)，操作使用B形式化方法的工業(yè)工具軟件，常用于需達(dá)到SIL3和SIL4功能安全級(jí)別的復(fù)雜系統(tǒng)的建模與驗(yàn)證，如由阿爾斯通和西門(mén)子等開(kāi)發(fā)的地鐵信號(hào)系統(tǒng)等。