技術領域

本發明涉及混成系統的可達性分析領域，具體而言涉及一類非線性混成系統的建模與面向路徑的可達性分析方法。

背景技術

混成系統(Hybrid?System)是一類同時具有離散和連續行為特征的復雜系統。在現實生活中,特別是航天、軍工、機械制造等嵌入式相關領域,混成系統均以核心控制器的形式大量存在，并發揮著至關重要的作用。因此,該系統的正確性驗證就有著特別重要的現實意義。當前,相關科研工作者主要采用混成自動機(Hybrid?Automata)來為混成系統建模。一個混成自動機的運行既包含狀態的離散變化，又包含狀態的連續變化,因此,相應的模型檢驗問題十分困難。工業領域大部分的混成系統都是非線性的，至今還沒有很好的驗證方法。

目前混成系統的研究主要都集中在線性混成系統領域，對其性質的驗證主要集中在可達性分析上。傳統的基于符號模型檢驗的相關技術和工具，大多是采用多面體計算來求解系統相應的可達性狀態集，但是此方法的復雜度是指數級的，只能應用于小規模系統。近年來，有界模型檢驗(Bounded?Model?Checking,簡稱BMC)技術被提出并得到了廣泛的應用。其主要思想是將有界可達性問題編碼為由命題變量和線性數學約束布爾組合而成的可滿足性問題，然后采用SMT（Satisfiability?Modulo?Theories）求解器進行求解，從而尋找給定步長內可達相應目標的路徑。由于此方法需要在檢驗前將特定步長內的所有行為編碼為一個約束集，所以編碼后問題的規模會隨著步長大小和系統變量數目呈指數級增長，從而限制問題的可解決規模；除此以外，雖然線性混成系統的可達性問題可以通過一定的編碼方式使用SMT方法加以解決，但是編碼本身是一項非常復雜的工作，目前沒有任何相應的支撐工具來完成此項工作。

對于應用較為廣泛的非線性混成系統，目前并沒有有效的工具對其進行可達性分析。少數的研究工作采用的是抽象或者過近似的方法，如非線性可達性驗證工具CheckMate采用的就是多面體過近似的方法來計算可達狀態集。

發明內容

針對現有技術的缺陷和不足，本發明的目的在于提供一類非線性混成系統的建模與面向路徑的可達性分析方法，對于一類特定的非線性系統的可達性問題能夠給出自動化的判定過程，并保證結果是精確的。

為達成上述目的，本發明的技術方案是：一類非線性混成系統的建模與面向路徑的可達性分析方法，該方法包括如下步驟：

步驟1：用非線性混成自動機對非線性混成系統進行建模：對于混成系統的連續狀態變化，用混成自動機的節點描述；對于混成系統的離散狀態變化，用混成自動機節點之間的狀態遷移來描述；其中，初始節點描述混成自動機的初始狀態；

步驟2：判斷非線性混成自動機的凸性混成；當混成自動機每一個節點上的狀態空間都為凸集時，稱該混成自動機為凸性混成自動機；

步驟3：若為凸性混成自動機，則根據規則將待驗證可達性問題編碼為凸規劃問題；

步驟4：求解編碼后的凸規劃問題；

步驟5：若問題可解，則說明當前求解路徑滿足可達性規約；否則，分別判斷凸性混成自動機是否屬于以下子類：線性流凸性混成自動機，要求凸性混成自動機所有節點上的流條件（Flow?Condition）都是線性的，也即是自動機中所有連續狀態變化的變化率都是線性的；單調不變式凸性混成自動機，要求凸性混成自動機上的不變式f(x)對于時間變量t都是單調的；

步驟6：若凸性混成自動機屬于上述子類中的任何一個，則說明當前求解路徑不滿足可達性規約；否則問題不可判定，放棄求解。

進一步，步驟3中：對于凸性混成自動機，將其編碼為凸規劃問題進行求解，給出半判定過程判定可達性：對于編碼后的凸規劃問題，若該問題有解，則對應的路徑滿足可達性規約；若該問題無解，則無法得到路徑是否滿足可達性規約；針對凸性混成自動機的兩個特殊子類，給出判定過程。兩個特殊子類：一類為線性流凸性混成自動機；另一類為單調不變式凸性混成自動機。

進一步，步驟4所描述的求解方法為得到凸規劃問題后，調用凸規劃求解器，如CVX等，對問題進行求解。

對于凸性混成自動機的一條路徑以及相應的可達性規約，通過編碼規則將它們轉化為凸規劃約束集，相應路徑的可達性可以通過凸規劃約束集的可滿足性得到。

由以上技術方案可知，本發明的一類非線性混成系統的建模與面向路徑的可達性分析方法，給出了用非線性混成自動機對非線性混成系統進行建模的方法，然后給出了將凸性混成自動機編碼為凸規劃問題的具體規則，最后給出了凸性混成自動機的可達性判定過程。