[發(fā)明專(zhuān)利]一種基于SoaML的云應(yīng)用正確性驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201310226221.6
• 申請(qǐng)日: 2013-06-07
• 公開(kāi)（公告）號(hào): CN103281329A
• 公開(kāi)（公告）日: 2013-09-04
• 發(fā)明（設(shè)計(jì)）人: 李必信;耿國(guó)清;王璐璐;陶傳奇;蘭陽(yáng)陽(yáng);司靜文
• 申請(qǐng)（專(zhuān)利權(quán)）人: 東南大學(xué)
• 主分類(lèi)號(hào): H04L29/06
• 分類(lèi)號(hào): H04L29/06;H04L29/08
• 代理公司: 南京瑞弘專(zhuān)利商標(biāo)事務(wù)所(普通合伙) 32249
• 代理人: 楊曉玲

技術(shù)領(lǐng)域

本發(fā)明屬于云計(jì)算的驗(yàn)證領(lǐng)域，涉及一種基于SoaML的云應(yīng)用正確性驗(yàn)證方法。

背景技術(shù)

云計(jì)算是分布式計(jì)算、并行計(jì)算和網(wǎng)格計(jì)算的進(jìn)一步發(fā)展，它描述了一種基于互聯(lián)網(wǎng)的新的IT服務(wù)增加、使用和交付模式，通常涉及通過(guò)互聯(lián)網(wǎng)來(lái)提供動(dòng)態(tài)易擴(kuò)展而且經(jīng)常是虛擬化的資源。云應(yīng)用是基于云計(jì)算思想實(shí)現(xiàn)的、部署在云環(huán)境中的軟件系統(tǒng)。云應(yīng)用往往應(yīng)用于一些對(duì)性能要求很高的領(lǐng)域，此類(lèi)系統(tǒng)投入使用后必須保證連續(xù)運(yùn)行，因此保障系統(tǒng)的正確性就顯得極為重要。測(cè)試和驗(yàn)證是保障軟件質(zhì)量的重要方法，但是在云應(yīng)用環(huán)境下，測(cè)試技術(shù)面臨著代價(jià)昂貴且操作難度極大等問(wèn)題，而形式化的驗(yàn)證方法就可以彌補(bǔ)這種不足。

越來(lái)越多的形式化驗(yàn)證方法及工具應(yīng)用于云應(yīng)用的驗(yàn)證，其中基于模型檢驗(yàn)（Model?Checking）的簡(jiǎn)單進(jìn)程元語(yǔ)言解釋器SPIN能有效準(zhǔn)確地表示云應(yīng)用的特征且適應(yīng)云應(yīng)用的驗(yàn)證工作。但是由于其支持的建模語(yǔ)言PROMELA難以進(jìn)行通用直觀的建模工作，特別在云應(yīng)用設(shè)計(jì)階段難以體現(xiàn)設(shè)計(jì)的一般化。本發(fā)明針對(duì)PROMELA語(yǔ)言的缺陷，使用SoaML對(duì)云應(yīng)用進(jìn)行建模，提出一種將SoaML中的ServiceInterface模型轉(zhuǎn)換為PROMELA的模型轉(zhuǎn)換方法，利用轉(zhuǎn)換得到的PROMELA進(jìn)行云應(yīng)用的形式化驗(yàn)證。將通用的模型轉(zhuǎn)換為形式化的模型進(jìn)行驗(yàn)證也是軟件工程領(lǐng)域研究的熱點(diǎn)。SoaML是UML的一種擴(kuò)展，彌補(bǔ)了UML沒(méi)有精確語(yǔ)義和很難描述云應(yīng)用的不足，且同時(shí)保持了UML通用直觀的特性。

發(fā)明內(nèi)容

技術(shù)問(wèn)題：本發(fā)明提供一種既可以很好地對(duì)通用建模語(yǔ)言所建的云應(yīng)用模型進(jìn)行驗(yàn)證，又彌補(bǔ)了PROMELA不夠通用、一般化的弱點(diǎn)的基于SoaML模型轉(zhuǎn)換的云應(yīng)用正確性驗(yàn)證方法。

技術(shù)方案：本發(fā)明的基于SoaML模型轉(zhuǎn)換的云應(yīng)用正確性驗(yàn)證方法，首先利用SoaML中的ServiceInterface方法對(duì)云應(yīng)用進(jìn)行建模，再進(jìn)行自動(dòng)模型轉(zhuǎn)換為SPIN支持的模型PROMELA，然后生成PROMELA代碼，并結(jié)合SoaML中的ServiceContract對(duì)應(yīng)的LTL代碼作為SPIN的輸入。

本發(fā)明的基于SoaML的云應(yīng)用正確性驗(yàn)證方法，包括如下步驟：

步驟1）建立給定的ServiceInterface元模型到PROMELA元模型的同態(tài)映射；

步驟2）將給定的ServiceInterface狀態(tài)機(jī)采用層次自動(dòng)機(jī)來(lái)描述，即以一個(gè)四元組SM＝＜＜S,H＞,E,T,D＞來(lái)表示ServiceInterface狀態(tài)機(jī)，其中＜S,H＞表示一個(gè)狀態(tài)層次，S是有限狀態(tài)集合，H是子狀態(tài)關(guān)系，E是有限狀態(tài)集合，T是有限轉(zhuǎn)換集合，D是缺省狀態(tài)集合。

步驟3）定義ServiceInterface狀態(tài)機(jī)的活動(dòng)狀態(tài)配置C∈2^S和事件隊(duì)列Q，活動(dòng)狀態(tài)配置C為某一時(shí)刻ServiceInterface狀態(tài)機(jī)所有活動(dòng)狀態(tài)的集合，事件隊(duì)列Q為觸發(fā)事件的隊(duì)列；

步驟4）定義一個(gè)對(duì)偶<C，Q>，用以表示ServiceInterface狀態(tài)機(jī)的活動(dòng)狀態(tài)配置C與事件隊(duì)列Q的格局；

步驟5）定義對(duì)偶<C,Q>轉(zhuǎn)換的約束，

(1)若substates(s)≠Φ，則kind(s)∈{composite,orthogonal};

(2)若kind(s)＝orthogonal，則#substates(s)≥2，并且對(duì)于所有s的后繼節(jié)點(diǎn)s′，

都有kind(s′)＝composite;

(3)若kind(s)＝composite，則#{s∈substates(s)|kind(s′)＝initial}≤1。

(4)kind(source(t))≠final

(5)kind(target(t))≠initial

(6)若kind(source(t)){initial,fork,join}，則guard(t)＝true;

(7)若kind(source(t))＝initial，則target(t)是非偽狀態(tài)(non-pseudostate);

(8)若kind(source(t))＝initial，則container(target(t))＝container(source(t));

(9)若kind(source(t))＝initial，則effect(t)＝skip;

(10)若kind(source(t))＝fork，則target(t)是偽狀態(tài);