我應該使用計算機輔助驗證工具嗎？

Question

我有興趣證明某些機器人控制器沒有達到任何故障狀態，我將通過一組謂詞來定義它。我知道有開源軟件工具可以實現這一點。例如，我聽說BLAST（伯克利懶惰抽象軟件驗證工具），但是你是否知道任何其他可能更容易使用和/或更具針對性的特定應用程序？

您是否曾經在您的項目中使用過BLAST或其他此類工具？您認爲這些好處大於部署此類工具所需的努力嗎？

Answer 1

您可能會感興趣Frama-C有用。

對於非Frama-C開發人員的評估，請參閱these two articles。一些開發安全關鍵代碼的工程師（例如DO-178B等級A）已經發現了基於最弱先決條件技術worth the investment的正式註釋和分析，但是傳統測試對他們而言非常昂貴。最後一個鏈接是關於Caveat，Frama-C打算在適當時候更換的閉源分析器。

你的問題聽起來好像你可能會欣賞Frama-C的Aoraï插件。

無論你是否花時間花在你的案件上，可能更多的是你是否考慮瞭解這些技術是一種快樂還是一件苦差事。