基于KeY的程序分析和驗證

夏新凱+陳冬火

摘要：可信性是各安全攸關領域軟件的基礎要求，例如航空航天飛行器控制軟件、核電站控制軟件和交通控制管理軟件等，基于形式化方法的程序驗證和分析是確保軟件正確，具有可信性的重要手段。相比軟件測試，基于定理證明的程序驗證具有語法和語義的嚴格性，和屬性相關的完備性。本文對程序形式化Hoare語義規(guī)約和相關的程序邏輯推理規(guī)則系統(tǒng)進行了詳細的討論?；谛问交炞C平臺KeY，采用完全自動化和交互式兩種方法，對具有一定規(guī)模的，含有循環(huán)結構，并且具有實際意義的程序進行驗證。研究證明過程的具體證明策略和方法，尤其是關于循環(huán)不變式的規(guī)約方法；對KeY的證明效率，先進性和局限性進行評估。endprint