[發明專利]一種構件系統建模及其動態演化一致性驗證方法

有效

• 申請號: 201710990872.0
• 申請日: 2017-10-23
• 公開（公告）號: CN107817970B
• 公開（公告）日: 2021-12-17
• 發明（設計）人: 李彤;鄭明;林英;謝仲文;秦江龍;莫啟;周小煊;李響;明利;鄭交交;楊真諦;王曉芳;成蕾
• 申請（專利權）人: 云南大學
• 主分類號: G06F8/20
• 分類號: G06F8/20;G06F11/36
• 代理公司: 昆明金科智誠知識產權代理事務所(普通合伙) 53216
• 代理人: 胡亞蘭

1.一種構件系統建模及其動態演化一致性驗證方法，其特征在于，所述構件系統建模及其動態演化一致性驗證方法包括以下步驟：

應用進程代數構造構件模型，并在構造的構件模型基礎上得到粗粒度的構件系統；根據構件系統及構件系統狀態的變化，進行構件系統外部行為的提取；基于弱互模擬理論定義構件系統動態演化一致性驗證準則；提取演化前后構件系統的行為，轉換成便于Pi演算自動工具MWB識別的格式，并進行行為一致性驗證；

構件系統外部行為的提取包括：

先將構件系統狀態及狀態轉換的動作序列用圖Graph的節點為構件系統的狀態節點；

初始化圖Graph，并將初始狀態節點Start入棧；

進入while循環，在循環中，查看棧頂狀態節點s在Graph圖中是否到達、入棧、且沒有從這個節點s出發訪問過的狀態節點；如果有，則將找到的這個狀態節點入棧；如果沒有，彈出棧頂狀態節點s；當棧頂元素為終點狀態時，打印輸出棧中元素，彈出棧頂狀態節點；

重復執行While循環直至棧為空，則圖Graph中所有從開始狀態節點出發到終點狀態節點的所有的動作序列都被找到；

所述基于弱互模擬理論定義構件系統動態演化一致性驗證準則中，弱互模擬包括：

PA上的某二元關系B為弱互模擬關系，當且僅當：無論何時，若有(E₁,E₂)∈B，則對所有操作而言，下列兩個條件同時滿足：

(1)若則存在E₂′，且(E₁',E₂')∈B；

(2)若則存在E₁′，且(E₁',E₂')∈B；

弱互摸擬關系的集合為觀察等價關系，表示為E₁≈_BE₂，其中表示忽略動作中τ的影響，若a＝τ，則其中，ε表示空操作序列，否則

2.如權利要求1所述的構件系統建模及其動態演化一致性驗證方法，其特征在于，

所述構件模型包括請求服務接口和提供服務接口；構件模型的接口的個數為k，其中，0≤k≤n，且構件模型的接口存在服務接口到請求接口和請求接口到另一請求接口的內部連接關系；

所述粗粒度的構件系統包括：

構件系統為一個四元組：其中：

N_M：N_M為構件系統的名稱；

是構件對象組成的集合；

L_M：表示有窮的構件對外連接集，體現構件系統中構件與構件之間的組裝連接信息，其中每一對構件連接l_i∈L_M定義三元組l_i＝C_N,Ite_i,LC_i，其中，

C_N：連接關系中的一個構件模型名稱；

Ite_i：表示相連構件模型之間的接口；

LC_i：表示構件C_N與構件系統中相連接的構件；

S_M：S_M表示構件系統的狀態，S_M＝{s₁,s₂,…,s_n}，其中s_i∈S_Ci,0≤i≤n，S_Init為初始化狀態，S_Fina為終止狀態。

3.如權利要求1所述的構件系統建模及其動態演化一致性驗證方法，其特征在于，所述轉換成便于Pi演算自動工具MWB識別的格式，包括：首先根據構件系統外部行為序列提取算法將外部行為提取出來，然后根據MWB工具的格式將演化前后構件系統的行為寫成特定的滿足MWB格式的行為序列。

4.一種構件系統，其特征在于，所述構件系統執行權利要求1～3任意一項所述構件系統建模及其動態演化一致性驗證方法。