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

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

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

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