云應(yīng)用的建模與驗(yàn)證方法基于SoaML和模型檢驗(yàn)的云應(yīng)用正確性驗(yàn)證.pdf

1、云計(jì)算是伴隨互聯(lián)網(wǎng)的蓬勃發(fā)展應(yīng)運(yùn)而生的一種新型計(jì)算方式，它突破了傳統(tǒng)計(jì)算的局限，增強(qiáng)了當(dāng)下急需的計(jì)算能力，同時(shí)又提供了靈活的可擴(kuò)展性。云應(yīng)用是基于云計(jì)算思想實(shí)現(xiàn)，并部署在云計(jì)算環(huán)境中的軟件系統(tǒng)。云應(yīng)用大多應(yīng)用于一些對(duì)性能要求很高的領(lǐng)域，因此保障系統(tǒng)的正確性就顯得極為關(guān)鍵。本文重點(diǎn)關(guān)注云應(yīng)用與用戶、云應(yīng)用之間和云應(yīng)用內(nèi)部的交互正確性。測(cè)試和驗(yàn)證是保障軟件正確性的主要方法，但是在云環(huán)境下，測(cè)試技術(shù)面臨著代價(jià)昂貴且操作難度極大等問(wèn)題。形式化的

2、驗(yàn)證方法規(guī)避了上述不足，因而適用于云應(yīng)用的正確性保障工作。
　　基于模型檢驗(yàn)的驗(yàn)證工具SPIN能有效地應(yīng)用于云應(yīng)用的驗(yàn)證。但是其支持的建模語(yǔ)言PROMELA卻難以進(jìn)行通用直觀的建模工作，特別在云應(yīng)用設(shè)計(jì)階段難以體現(xiàn)設(shè)計(jì)的一般化。SoaML是UML的一種擴(kuò)展。后者是一種標(biāo)準(zhǔn)建模語(yǔ)言，軟件行業(yè)的廣泛實(shí)踐已經(jīng)證明了它在系統(tǒng)建模中的有效性和通用性。SoaML秉承了UML通用直觀的特性，同時(shí)具備了更高的抽象層次。它彌補(bǔ)了UML沒(méi)有精確語(yǔ)義和

3、很難描述云應(yīng)用的不足，可用于云應(yīng)用的建模。本文首先采用SoaML對(duì)云應(yīng)用進(jìn)行建模。然后，針對(duì)SoaML中的ServiceInterface模型的特點(diǎn)，采用層次自動(dòng)機(jī)來(lái)描述ServiceInterface，再根據(jù)自動(dòng)機(jī)的語(yǔ)義將其轉(zhuǎn)換為PROMELA。同時(shí)，將SoaML中的ServiceContract模型采用線性時(shí)序邏輯描述。最后將轉(zhuǎn)換而來(lái)的PROMELA和線性時(shí)序邏輯公式輸入SPIN中就可以進(jìn)行云應(yīng)用的自動(dòng)驗(yàn)證。實(shí)驗(yàn)表明，該方法可以有效