《狀態轉換系統的格值量化驗證方法研究》是依託華東師範大學，由張敏擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：狀態轉換系統的格值量化驗證方法研究
- 項目類別：青年科學基金項目
- 項目負責人：張敏
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
形式化驗證是使用數學方法確保計算機軟硬體系統的正確性和可靠性。常用的形式化驗證方法是互模擬等價驗證和模型檢測技術。經典的互模擬等價驗證和模型檢測技術是在二值邏輯上展開的。近年來，大家開始關注非二值情形的形式化驗證方法研究，逐步形成了量化驗證理論，包括數值量化驗證方法和非數值量化驗證方法。本項目提出格值互模擬理論和格值模型檢測方法，形成一種新的非數值（格值）量化驗證理論，其研究成果具有重要的理論意義和一定的套用價值。..在前期工作基礎上，本項目主要研究以下兩部分內容：(一)建立格值互模擬理論，探討格值互模擬關係的重要性質，為分析系統滿足其規範的(格值)量化程度提供理論依據；(二)提出格值模型檢測方法，研究格值模型檢測中的可判定性問題，為自動量化驗證技術提供理論基礎。
結題摘要
近年來，非二值情形的形式化驗證方法研究成為研究熱點，逐步形成了量化驗證理論，包括數值量化驗證方法和非數值量化驗證方法。本項目提出格值互模擬理論和格值模型檢測方法，形成一種新的非數值（格值）量化驗證理論，其研究成果具有重要的理論意義和一定的套用價值。經過三年的研究，我們得到了以下三部分的研究成果：(一)建立格值互模擬理論，探討格值互模擬關係的重要性質，為分析系統滿足其規範的(格值)量化程度提供理論依據；(二)提出格值模型檢測方法，研究格值模型檢測中的可判定性問題，為自動量化驗證技術提供理論基礎。（三）開發實現了一個有效的量化驗證工具SPAC及領域內的量化評估工具，為理論的實際套用的建立了一套可行性方案。
