《時間敏感下推系統可達性的驗證問題》是依託上海交通大學，由李國強擔任項目負責人的面上項目。
基本介紹
- 中文名：時間敏感下推系統可達性的驗證問題
- 項目類別：面上項目
- 項目負責人：李國強
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
時間敏感下推系統對具有實時要求的程式分析和系統驗證具有重要的理論和套用價值。其中，可達性問題是這個系統的重要性質之一，許多驗證問題可以通過可達性檢測來解決。目前，尚未有時間敏感下推系統可達問題可判定一般性結論，也沒有高效的驗證工具。為此，首先，擬採用將2計數器機器規約到該系統的方式，證明一般情況下時間敏感下推系統的可達性不可判定，並通過將各種適於程式分析和系統驗證的時間敏感下推系統子模型規約到良結構下推自動機，來證明這些子模型可達性可判定，同時，研究並發時間敏感下推系統可達性的判定問題，並將之套用於多執行緒程式分析；其次，將時間敏感下推系統的時間區間權重化，並通過規約此類模型至權重下推自動機的方式來高效實現出模型檢測工具；最後，通過研究實現時間正則任務系統的可調度分析器,驗證時間敏感下推系統模型檢測工具的效用，並且解決任務系統中執行時間不固定的條件下，任務系統可調度性是否可判定的開放問題。
結題摘要
時間敏感下推系統對具有實時要求的程式分析和系統驗證具有重要的理論和套用價值。其中，可達性問題是這個系統的重要性質之一，許多驗證問題可以通過可達性檢測來解決。本研究有如下成果：其一，研究時間敏感下推系統在不同類型時鐘，如公有時鐘、私有時鐘、停凍時鐘、可調整時鐘，以及在不同類型約束下，如對角線時間約束、不變數約束，模型的可達性的可判定與不可判定的界。其二，通過上近似的方法高效實現了時間敏感下推系統的驗證工具，並且完成了嵌入式作業系統OSEK/VDX的安全性驗證。其三，通過研究實現時間正則任務系統的可調度性和安全性的分析,驗證時間敏感下推系統驗證工具的效用。
