[發明專利]基于時態邏輯的微控制器運行時驗證系統

在審

• 申請號: 201710138988.1
• 申請日: 2017-03-09
• 公開（公告）號: CN106951367A
• 公開（公告）日: 2017-07-14
• 發明（設計）人: 史建琦;胡志成;黃滟鴻;李昂;方徽星
• 申請（專利權）人: 華東師范大學;上海豐蕾信息科技有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京辰權知識產權代理有限公司11619
• 代理人: 郎志濤

1.一種基于時態邏輯的微控制器運行時驗證系統，其特征在于，包括：

事件接收模塊，用于實時接收并記錄微控制器執行的每個事件；

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

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

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

2.如權利要求1所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述事件接收模塊為JTAG接口或者協處理器接口，其將記錄的微控制器執行的每個事件保存到日志文件中。

3.如權利要求1所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述事件預處理模塊還將所述原子命題添加到原子命題集當中。

4.如權利要求1所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述用戶編輯模塊包括原子命題集編輯單元和LTL公式編輯單元。

5.如權利要求4所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述原子命題集編輯單元顯示一個原子命題集列表，用戶可以通過編輯所述列表對原子命題集中的原子命題進行編輯，刪除不合理或者無用的原子命題，也可以添加新的原子命題到原子命題集中。

6.如權利要求4所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述LTL公式編輯單元提供LTL公式編輯窗口，以供用戶編寫LTL公式。

7.如權利要求6所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述TLT公式編輯窗口設定LTL公式輸入規則，可以自動屏蔽一些非法輸入，同時可以對用戶輸入的LTL公式進行合法性檢查，高亮出不合法的部分。

8.如權利要求6或7所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述LTL驗證模塊將LTL公式編輯單元輸出的LTL公式以及事件預處理模塊輸出的事件序列字符串作為輸入，通過采用LTL驗證算法來驗證事件序列字符串是否滿足上述LTL公式編輯單元輸出的LTL公式，并將驗證結果反饋給微控制器。

9.如權利要求8所述的基于時態邏輯的微控制器運行時驗證系統，其特征在于，所述LTL驗證算法為傳統LTL算法，通過將LTL公式轉換為büchi自動機，來判斷事件序列字符串是否可以被büchi自動機所接受。