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

在審

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

本發明公開了一種基于量化時序約束的智能家居運行時驗證方法，基于量化時序約束，定義用戶執行自主活動時的環境需求；基于度量時序邏輯，將定義的環境需求轉化為時序邏輯公式，并進行性質規約，生成屬性監控器；通過傳感器，獲取智能家居系統中環境屬性的屬性值，并進行預處理，得到運行時狀態數據；基于S?Taliro工具中的驗證算法，結合智能家居系統的運行時狀態數據以及屬性監控器，驗證智能家居系統的運行時狀態是否滿足需求；根據驗證結果，觸發智能家居設備執行不同操作，如果滿足需求，則智能家居系統維持當前狀態，否則根據預定義的策略，改變智能家居設備的運行狀態。

技術領域

本發明涉及智能家居運行時驗證領域，具體涉及了一種基于量化時序約束的智能家居運行時驗證方法。

背景技術

隨著現代環境感知技術、物聯網技術的發展，智能家居新技術及其應用得到了蓬勃發展。然而，在實際運行過程中，某些物理環境有可能會對智能家居的程序造成影響。為了保證智能家居運行的安全性和可靠性，有必要對系統運行期間進行監控，及時檢測系統的運行錯誤，幫助相關人員積極做出應對。目前，針對智能家居系統的驗證主要采用靜態驗證的方式，如通過窮盡遍歷模型狀態空間進行驗證，能夠明確地給出驗證結果，即模型是否符合規約。然而，面對智能家居軟件不斷增加的復雜性和相關硬件體系結構的不確定性，模型檢驗技術會遇到狀態空間爆炸問題，無法很好地給出驗證結果。

發明內容

本發明的目的在于提供一種基于量化時序約束的智能家居運行時驗證方法。

實現本發明目的的技術解決方案為：一種基于量化時序約束的智能家居運行時驗證方法，包括如下步驟：

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

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

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

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

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

進一步的，步驟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]內，一直滿足約束，若無時間限制，則表示總是有效。

進一步的，步驟2中，基于度量時序邏輯，將定義的環境需求轉化為時序邏輯公式，并進行性質規約，生成屬性監控器，實現對環境屬性的監控，具體方法為：

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