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

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

第28章 可信軟件驗證技術

可信軟件的驗證技術

·形式化建模與方法

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

·可信軟件驗證工具

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

________。

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