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

有效

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

本發明屬于軟件開發技術領域，公開了一種構件系統建模及其動態演化一致性驗證方法，應用進程代數構造構件模型，并在此基礎上得到粗粒度的構件系統；根據構件系統及其狀態的變化，進行構件系統外部行為的提取，基于弱互模擬理論定義構件系統動態演化一致性驗證準則；提取演化前后構件系統的行為，轉換成便于Pi演算自動工具MWB識別的格式進行行為一致性驗證。本發明基于構件間的交互及組合關系構建了更粗粒度的便于演化前后行為一致性分析的構件系統；提出構件系統外部行為序列提取算法，實現了構件系統外部行為序列提取的自動化；基于Milner的弱互模擬理論提出了構件系統演化前后行為一致性的驗證準則。

技術領域

本發明屬于軟件開發技術領域，尤其涉及一種構件系統建模及其動態演化一致性驗證方法。

背景技術

隨著軟件開發技術的發展，基于構件式的軟件開發方法已經比較成熟。一般來說，基于構件式的軟件工程(component-basedsoftwareengineering,CBSE)是將所需的構件通過集成組裝成最終所需的系統。隨著系統的維護以及用戶需求的改變，構件的增加、刪除和修改無法避免，演化后構件系統的行為是否偏離演化前的構件系統行為是判斷構件系統動態演化正確與否的本質標準，也是保證動態演化實施可靠性的重要條件，即構件在動態演化前后，與其它構件之間可觀察的交互行為必須保持一致。

為了驗證軟件系統演化前后的系統一致性問題，國內外學者針對面向動態演化的構件建模及演化前后系統行為一致性的驗證做了大量的分析工作。如文獻給出了基于構件行為協議的構件式軟件系統中構件可替換的必要條件，至于替換后的構件系統與替換前的構件系統是否一致，作者并沒有給出相應的驗證替換前后系統一致性的方法，因此本發明提出了一種基于進程代數建模的構件系統演化前后一致性驗證的方法。文獻基于Petri網形式化工具對構件進行建模并在系統行為層面加入一致性約束，這樣在保證原來系統功能行為正確的前提下增加了靈活性，但它不具有將多個petri子網構件行為計算組合并成一個大的petri網構件系統行為的標準并發操作，使得構件演化前后的一致性標準較低，很難準確地去驗證演化后系統的一致性，本發明基于進程代數對構件和構件系統進行建模，使得其不僅具有嚴格的形式化語義，同時還具備了通過并發操作符將多個構件的行為計算組合成更粗粒度的構件系統的行為。文獻和文獻基于進程代數構建構件模型，形式化描述了構件及其對外交互協議，雖然給出了演化前后行為一致性驗證規則，但缺少對構件外部交互行為提取和具體的構件行為一致性標準，因此本發明提出了一種能夠對構件系統模型外部行為序列提取算法和基于弱互模擬理論的一致性驗證準則。文獻基于時間自動機模型對軟件演化前后狀態行為進行建模，利用時間自動機模型驗證工具UPPAAL對系統的安全性規約和活性規約進行了驗證，但時間自動機無法對構件系統內部的活動進行精細地刻畫，如不能有效地描述多個活動的并發執行等，雖然采用時間自動機模型也可以對構件之間的行為交互協議進行建模，但以時間自動機模型表示的構件的行為交互只能支持相關性質的檢查，并不能支持等價理論，因而也就不支持構件之間的相似性分析。本發明之所以采取進程代數來對構件進行建模正是因為進程代數能夠對構件系統內部多個活動的并發進行有效的支持，并能將多個構件的行為計算組合成總行為，在弱互模擬的理論上支持相似性的分析，因此能夠支持構件系統動態演化前后的一致性的驗證。

綜上所述，現有技術存在的問題是：針對構件系統動態演化后一致性保持問題，目前尚缺乏被普遍接受的標準，本發明基于Milner的弱互模擬理論提出了構件系統動態演化前后的行為一致性標準，另對于構件系統的行為提取方面，本文提出了構件系統模型外部行為序列的提取算法，實現了構件系統模型外部行為序列提取的自動化。

發明內容

針對現有技術存在的問題，本發明提供了一種構件系統建模及其動態演化一致性驗證方法。

本發明是這樣實現的，一種構件系統建模及其動態演化一致性驗證方法，所述構件系統建模及其動態演化一致性驗證方法包括以下步驟：