[發明專利]一種基于量化時序約束的智能家居運行時驗證方法

在審

• 申請號: 202210023752.4
• 申請日: 2022-01-10
• 公開（公告）號: CN114676003A
• 公開（公告）日: 2022-06-28
• 發明（設計）人: 李晅松;張智慧
• 申請（專利權）人: 南京理工大學
• 主分類號: G06F11/22
• 分類號: G06F11/22
• 代理公司: 南京理工大學專利中心 32203
• 代理人: 封睿

1.一種基于量化時序約束的智能家居運行時驗證方法，其特征在于，包括如下步驟：

步驟1，基于量化時序約束，定義用戶執行自主活動時的環境需求；

步驟2，基于度量時序邏輯，將定義的環境需求轉化為時序邏輯公式，并進行性質規約，生成屬性監控器；

步驟3，通過傳感器，獲取智能家居系統中環境屬性的屬性值，并進行預處理，得到運行時狀態數據；

步驟4，基于S-Taliro工具中的驗證算法，結合智能家居系統的運行時狀態數據以及屬性監控器，驗證智能家居系統的運行時狀態是否滿足需求；

步驟5，根據驗證結果，觸發智能家居設備執行不同操作，如果滿足需求，則智能家居系統維持當前狀態，否則根據預定義的策略，改變智能家居設備的運行狀態。

2.根據權利要求1所述的基于量化時序約束的智能家居運行時驗證方法，其特征在于，步驟1中，基于量化時序約束，定義用戶執行自主活動時的環境需求，具體方法為：

11)根據時間區間理論，將時間約束描述為區間的形式：Time:[a,b]，其中a,b分別表示需求需要滿足的最早時間點和最晚時間點，其中ab；

12)采用二元組的形式：Request:actType,req，定義需求，其中actType為用戶活動類型，req是對相關環境屬性約束的集合，且其為類比度量時序邏輯語法而定義的公式：req:＝pred|◇_[a,b]pred|□_[a,b]pred；

在req公式中，pred為環境屬性的約束，◇_[a,b]是帶有時間限制的“最終”運算符，表示在未來時間段[a,b]內，存在從某一時刻開始滿足約束，若無時間限制，則表示總是有效；□_[a,b]帶有時間限制的“總是”運算符，表示在未來時間段[a,b]內，一直滿足約束，若無時間限制，則表示總是有效。

3.根據權利要求1所述的基于量化時序約束的智能家居運行時驗證方法，其特征在于，步驟2中，基于度量時序邏輯，將定義的環境需求轉化為時序邏輯公式，并進行性質規約，生成屬性監控器，具體方法為：

21)利用度量時序邏輯MTL公式，將定義的環境需求Request轉化為為相應的時序約束邏輯公式，其中度量時序邏輯MTL公式為：

phi:＝p|(phi)|！phi|phi∨phi|phi∧phi|phi→phi|◇_[a,b]phi|□_[a,b]phi

其中p是一個用于描述相關性質的謂詞；！是邏輯關系詞“非”；∨是邏輯關系詞“或”；∧是邏輯關系詞“與”；→是邏輯關系詞“蘊含”；◇_[a,b]是帶有時間限制的“最終”運算符，表示在未來時間段[a,b]內，存在從某一時刻開始滿足約束，若無時間限制，則表示總是有效；□_[a,b]帶有時間限制的“總是”運算符，表示在未來時間段[a,b]內，一直滿足約束，若無時間限制，則表示總是有效；

根據上述邏輯，將定義的環境需求Request轉化為相應的時序約束邏輯公式phi，在phi中，相關環境屬性描述為MTL公式中的謂詞p；

22)對同一活動類型actType的邏輯公式phi進行匯總，得到時序約束邏輯公式集合Nature:{phi₁,phi₂,…,phi_n}；

23)對于邏輯公式集合Nature的每個phi公式，進行性質規約，生成屬性監控器Pred，對每個謂詞的約束進行形式化描述，實現謂詞到各自約束的映射，并指定監控位置，完成對環境屬性的監控。

4.根據權利要求1所述的基于量化時序約束的智能家居運行時驗證方法，其特征在于，步驟3中，通過傳感器，獲取智能家居系統中環境屬性的屬性值，并進行預處理，得到運行時狀態數據，具體方法為：

31)通過傳感器，獲取智能家居系統中環境屬性的屬性值，采用三元組的形式對其進行描述State:time,attribute,dataList，其中time為時間，attribute為屬性名，dataList為屬性值；

32)對于非數值型屬性值進行數值化，匯總屬性信息形成運行狀態表格Table:{state}，從而得到系統的運行時狀態數據。