技術領域

本發明主要涉及運行時驗證以及形式化驗證領域，尤其涉及基于時態邏輯的微控制器運行時驗證方法。

背景技術

隨著計算機科學技術的發展，越來越多的嵌入式系統滲入到人們的生活之中。嵌入式系統的安全關系到人們生活的方方面面，包括醫療、交通、教育等等。一旦這樣的系統受到攻擊，帶來的損失可能是巨大的甚至是不可估量的。而微控制器是所有嵌入式系統的心臟，保障微控制器的安全對嵌入式系統安全來說至關重要。

傳統的微控制器的特點是資源有限、指令集簡單、處理事件單一。隨著芯片技術的發展，現在的微控制器結構變得更為復雜，而且嵌入式系統也在逐漸地網絡化，使得微控制器面臨著更多的被攻擊可能性。如何保障微控制器的安全、穩定運行是一個值得深入研究的問題。

另外，運行時驗證技術是一種檢查系統的運行情況，判定系統是否符合給定的屬性或者規范的驗證技術。形式化驗證技術指的是采用形式化方法來對系統進行驗證的技術，判定系統是否滿足特定的形式規約。

目前，運行時驗證技術往往用于軟件系統的驗證，例如中國發明專利申請號為201510181988.0的發明專利申請，公開了一種可動態部署規則的Java程序運行時驗證系統，該系統運行于DiSL字節碼注入框架之上，包括驗證規則翻譯器、部署管理器以及運行時引擎三個步驟，所述驗證規則翻譯器用于將驗證規則定義文件翻譯成由事件注入代碼和規則驗證代碼組合成驗證代碼，所述部署管理器用于提供部署驗證代碼的相關用戶接口；所述運行時引擎用于根據接收的驗證代碼中事件注入代碼產生的事件序列，為每個監控對象維護一個事件序列，驗證事件注入代碼產生的事件序列是否與規則驗證代碼的事件序列相同，并根據驗證情況通過部署管理器對事件注入代碼進行實時部署優化。

然而，現有技術中沒有將運行時驗證技術和形式化驗證技術用于微控制器的驗證方法。傳統上來說，保障微控制器安全的做法是通過改善微控制器的設計、數據加密等等。目前的驗證方法較為復雜，而且成本較高，無法實現實時驗證。

發明內容

為解決以上問題，本發明提出了基于時態邏輯的微控制器運行時驗證方法，通過將微控制器所執行的事件序列轉換成由一串變量名表示的事件序列字符串，將微控制器需要滿足的性質用LTL公式進行描述，判斷事件序列字符串是否滿足給定的LTL公式，來實現微控制器的運行時驗證。

具體的，本發明提出了一種基于時態邏輯的微控制器運行時驗證方法，包括：

事件接收步驟，實時接收并記錄微控制器執行的每個事件；

事件預處理步驟，對事件接收步驟接收到的事件預處理，將事件轉換成一個個獨立的原子命題，然后為每個原子命題分配唯一的變量標識，建立上述變量標識與原子命題之間的一一映射，并輸出事件序列字符串；

用戶編輯步驟，給用戶提供編輯界面，以供用戶編輯原子命題以及LTL公式；

LTL驗證步驟，驗證所述微控制器執行所述事件序列字符串是否滿足用戶輸入的LTL公式。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述事件接收步驟將記錄的微控制器執行的每個事件保存到日志文件中。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述事件預處理步驟還將所述原子命題添加到原子命題集當中。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述用戶編輯步驟包括原子命題集編輯步驟和LTL公式編輯步驟。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述原子命題集編輯步驟顯示一個原子命題集列表，用戶可以通過編輯所述列表對原子命題集中的原子命題進行編輯，刪除不合理或者無用的原子命題，也可以添加新的原子命題到原子命題集中。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述LTL公式編輯步驟提供LTL公式編輯窗口，以供用戶編寫LTL公式。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述TLT公式編輯窗口設定LTL公式輸入規則，可以自動屏蔽一些非法輸入，同時可以對用戶輸入的LTL公式進行合法性檢查，高亮出不合法的部分。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述LTL驗證步驟通過采用LTL驗證算法來驗證事件序列字符串是否滿足上述LTL公式編輯步驟的LTL公式，并將驗證結果反饋給微控制器。

優選的，如上所述的基于時態邏輯的微控制器運行時驗證方法，所述LTL驗證算法為傳統的LTL算法，通過將LTL公式轉換為büchi自動機，來判斷事件序列字符串是否可以被büchi自動機所接受。