基于模型檢測的動態(tài)協(xié)同服務(wù)間的一致性驗證.pdf

1、近年來面向服務(wù)架構(gòu)（SOA）作為一種非常有前景的軟件開發(fā)技術(shù)，已經(jīng)吸引了越來越多的關(guān)注。SOA松散耦合的特性保證了服務(wù)的快速組合和動態(tài)配置，然而，與此同時也給系統(tǒng)的一致性和可靠性帶來了更多的挑戰(zhàn)。因此，在模型級上對服務(wù)協(xié)同的一致性和可靠性的驗證逐漸成為研究熱點，借此可以大大降低SOA應(yīng)用的開發(fā)風(fēng)險，節(jié)約企業(yè)的人力物力。
　　 統(tǒng)一建模語言(UML)已經(jīng)成為面向?qū)ο蠓治龊驮O(shè)計方法的代表，獲得了廣泛的關(guān)注。UML是一種統(tǒng)一的、便捷的

2、而且表達能力強的可視化建模語言，使其成為模型驅(qū)動式軟件開發(fā)過程中的核心技術(shù)，而缺乏精確的語義描述又使得UML難以驗證設(shè)計規(guī)范是否滿足系統(tǒng)需求。
　　 通過對服務(wù)協(xié)同概念及驗證方法的分析，本論文提出了一種基于SPIN模型檢測的動態(tài)協(xié)同服務(wù)間一致性的驗證方法。
　　 首先對UML順序圖進行了狀態(tài)屬性的擴展，增加了消息的進入狀態(tài)屬性，得到擴展順序圖（ESD），增強了UML順序圖面向系統(tǒng)動態(tài)行為的表達能力；其次，通過對基于契約的

3、服務(wù)協(xié)同和ESD語義的分析，形式化分析和描述了服務(wù)間的協(xié)同時序契約(CC)的概念，形式化定義了系統(tǒng)中服務(wù)動態(tài)行為一致性的概念，為服務(wù)間的協(xié)同協(xié)議提供了形式化支持；然后，選取UML狀態(tài)圖建模服務(wù)的動態(tài)行為，選取UML擴展順序圖建模服務(wù)間的協(xié)同時序契約，根據(jù)相應(yīng)的映射規(guī)則，將UML狀態(tài)圖建模的動態(tài)行為映射成驗證工具SPIN的建模語言Promela，將UML擴展順序圖建模的協(xié)同時序契約映射成LTL時態(tài)邏輯公式；利用模型驗證工具SPIN驗證映射