[發明專利]基于時態邏輯的微控制器運行時驗證方法在審
| 申請號： | 201710139008.X | 申請日： | 2017-03-09 |
| 公開（公告）號： | CN106933714A | 公開（公告）日： | 2017-07-07 |
| 發明（設計）人： | 史建琦;胡志成;黃滟鴻;李昂;方徽星 | 申請（專利權）人： | 華東師范大學;上海豐蕾信息科技有限公司 |
| 主分類號： | G06F11/26 | 分類號： | G06F11/26 |
| 代理公司： | 北京辰權知識產權代理有限公司11619 | 代理人： | 郎志濤 |
| 地址： | 200062 上*** | 國省代碼： | 上海;31 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 基于 時態 邏輯 控制器 運行 驗證 方法 | ||
1.一種基于時態邏輯的微控制器運行時驗證方法，其特征在于，包括：
事件接收步驟，實時接收并記錄微控制器執行的每個事件；
事件預處理步驟，對事件接收步驟接收到的事件預處理，將事件轉換成一個個獨立的原子命題，然后為每個原子命題分配唯一的變量標識，建立上述變量標識與原子命題之間的一一映射，并輸出事件序列字符串；
用戶編輯步驟，給用戶提供編輯界面，以供用戶編輯原子命題以及LTL公式；
LTL驗證步驟，驗證所述微控制器執行所述事件序列字符串是否滿足用戶輸入的LTL公式。
2.如權利要求1所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述事件接收步驟將記錄的微控制器執行的每個事件保存到日志文件中。
3.如權利要求1所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述事件預處理步驟還將所述原子命題添加到原子命題集當中。
4.如權利要求1所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述用戶編輯步驟包括原子命題集編輯步驟和LTL公式編輯步驟。
5.如權利要求4所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述原子命題集編輯步驟顯示一個原子命題集列表，用戶可以通過編輯所述列表對原子命題集中的原子命題進行編輯，刪除不合理或者無用的原子命題，也可以添加新的原子命題到原子命題集中。
6.如權利要求4所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述LTL公式編輯步驟提供LTL公式編輯窗口，以供用戶編寫LTL公式。
7.如權利要求6所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述TLT公式編輯窗口設定LTL公式輸入規則，可以自動屏蔽一些非法輸入，同時可以對用戶輸入的LTL公式進行合法性檢查，高亮出不合法的部分。
8.如權利要求6或7所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述LTL驗證步驟通過采用LTL驗證算法來驗證事件序列字符串是否滿足上述LTL公式編輯步驟的LTL公式，并將驗證結果反饋給微控制器。
9.如權利要求8所述的基于時態邏輯的微控制器運行時驗證方法，其特征在于，所述LTL驗證算法為傳統LTL算法，通過將LTL公式轉換為büchi自動機，來判斷事件序列字符串是否可以被büchi自動機所接受。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于華東師范大學;上海豐蕾信息科技有限公司，未經華東師范大學;上海豐蕾信息科技有限公司許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.17sss.com.cn/pat/books/201710139008.X/1.html，轉載請聲明來源鉆瓜專利網。
