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

軟考軟件評測師考試知識點填空檢測（28）內(nèi)容如下：

第28章 可信軟件驗證技術

可信軟件的驗證技術

·形式化建模與方法

形式化驗證技術：定理證明、________。

·可信軟件驗證工具

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

________。

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