基于時間護展的ASEHA的模型檢測技術(shù)研究.pdf

1、隨著技術(shù)的發(fā)展和人們需求的不斷提高,實時系統(tǒng)的復(fù)雜度在不斷地增長,為實時系統(tǒng)的開發(fā)帶來了巨大挑戰(zhàn)。本文在異步擴展層次自動機(Asynchronous Extended Hierarchical Automata, ASEHA)上,引入了時鐘變量,在遷移和位置上增加了時鐘約束,給出了一種具有時間擴展的ASEHA模型,有效降低了實時系統(tǒng)建模的復(fù)雜性,利用模型檢測工具UPPAAL,對 ATM(Automatic Teller Machine)

2、系統(tǒng)和旅游預(yù)訂票Web服務(wù)系統(tǒng)進行檢驗,驗證了系統(tǒng)無死鎖、可達性、活性、安全性等性質(zhì)。本文所取得的主要成果有:
　　(1)針對實時系統(tǒng),給出了一種基于時間擴展的ASEHA模型。將實時系統(tǒng)建模為具有時間擴展的ASEHA模型,以ATM系統(tǒng)為例闡述了建模過程,利用UPPAAL工具檢驗該系統(tǒng)的可達性等性質(zhì),最后驗證表明該模型是正確的、安全的。
　　(2)針對帶時間約束的組合W eb服務(wù)系統(tǒng),給出了一種模型檢測方法。將組合W eb服務(wù)

3、的描述語言BPEL4WS轉(zhuǎn)化成基于時間擴展的ASEHA語言,對組合Web服務(wù)建立形式化模型,采用模型檢測工具UPPAAL對系統(tǒng)的實時性和可信性進行驗證,從而保證了系統(tǒng)模型的實效性與安全性。
　　(3)基于本文提出的具有時間擴展的ASEHA對帶時間約束的組合Web服務(wù)系統(tǒng)驗證的方法,分析了旅游預(yù)訂票W eb服務(wù)系統(tǒng),給出了該系統(tǒng)的BPEL4WS描述語言轉(zhuǎn)化為時間擴展的ASEHA語言代碼和形式化定義描述,建立了基于時間擴展的ASEHA