時(shí)間約束條件下web服務(wù)組合的形式化分析與驗(yàn)證.pdf

1、隨著Web技術(shù)和商業(yè)應(yīng)用的快速發(fā)展，面向服務(wù)的計(jì)算(SOC)和面向服務(wù)的體系結(jié)構(gòu)(SOA)也已成為人們關(guān)注的焦點(diǎn)。由于兩者的出現(xiàn)，有效解決在分布以及異構(gòu)環(huán)境下軟件集成與復(fù)用。當(dāng)前，日益成熟的Web服務(wù)技術(shù)也為兩者提供了有效地技術(shù)支撐。Web服務(wù)是一種基于網(wǎng)絡(luò)的具有松耦合、獨(dú)立性強(qiáng)等特點(diǎn)的軟件構(gòu)件。服務(wù)是Web體系中交互的基本單位。由于單個(gè)Web服務(wù)的功能有限，web服務(wù)組合技術(shù)已成構(gòu)建電子商務(wù)應(yīng)用的主要方法之一。然而，如何確保在復(fù)雜環(huán)境

2、下的Web服務(wù)能夠保證軟件的質(zhì)量，滿足人們的預(yù)期呢？特別是限定服務(wù)的行為必須滿足給定的時(shí)間約束條件。形式化技術(shù)作為軟件質(zhì)量保證的一種重要方法。
　　本研究為適應(yīng)快速變化的商業(yè)環(huán)境，對(duì)商業(yè)應(yīng)用提出了實(shí)時(shí)性的要求。提出了一種形式化方法，用于分析與驗(yàn)證web服務(wù)組合的時(shí)間約束行為。首先，擴(kuò)展了Web服務(wù)接口描述語(yǔ)言，增加對(duì)時(shí)間約束的描述，然后定義一種時(shí)間行為自動(dòng)機(jī)，用于刻畫web服務(wù)組合的時(shí)間行為，最終利用模型驗(yàn)證技術(shù)來(lái)自動(dòng)驗(yàn)證這些行為