Uppaal時(shí)間自動(dòng)機(jī)規(guī)格說明到PVS時(shí)間自動(dòng)機(jī)模板的轉(zhuǎn)換.pdf

1、隨著計(jì)算機(jī)技術(shù)的飛速發(fā)展，實(shí)時(shí)系統(tǒng)(real-time system)的應(yīng)用日益廣泛。在實(shí)際應(yīng)用中，隨著實(shí)時(shí)系統(tǒng)規(guī)模不斷擴(kuò)大、功能不斷增強(qiáng)，導(dǎo)致實(shí)時(shí)系統(tǒng)運(yùn)行時(shí)軟件出現(xiàn)錯(cuò)誤的可能性也在增加。實(shí)時(shí)系統(tǒng)軟件運(yùn)行過程中出現(xiàn)的任何一點(diǎn)差錯(cuò)將會(huì)導(dǎo)致巨額經(jīng)濟(jì)損失、時(shí)間浪費(fèi)，甚至人員傷亡。為保證實(shí)時(shí)系統(tǒng)軟件的正確性和安全性，提高其運(yùn)行的可靠性，人們采取了許多的技術(shù)手段，其中形式化方法(fortmal methods)起到了重要的作用。 實(shí)時(shí)系統(tǒng)

2、驗(yàn)證工具Uppaal由瑞典的Uppsala大學(xué)和丹麥的Aalborg大學(xué)合作開發(fā)，它包括三個(gè)主要部分：編輯器、模擬器和驗(yàn)證器。PVS ( PrototypeVerification System)是一個(gè)由斯坦福研究機(jī)構(gòu)開發(fā)的原型驗(yàn)證系統(tǒng)。它包含規(guī)格說明語言、語法分析器、類型檢查器、證明器、規(guī)格說明庫和各種瀏覽工具。PVS規(guī)格說明語言是基于高階邏輯(higher order logic)的，有豐富的類型系統(tǒng)和相應(yīng)的類型檢查器，通過提供有效

3、的定理證明器來支持錯(cuò)誤檢測(cè)。時(shí)間自動(dòng)機(jī)是對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行分析的一種有效的形式化方法。 Uppaal作為一個(gè)用時(shí)間自動(dòng)機(jī)模型進(jìn)行建模、檢查、驗(yàn)證的可視化工具，操作起來非常方便。但是也有非常明顯的缺點(diǎn)。一是模型檢查的時(shí)間復(fù)雜度比較大。二是可能會(huì)產(chǎn)生幾乎所有基于時(shí)間自動(dòng)機(jī)的模型檢查工具都要面對(duì)的問題——狀態(tài)空間爆炸。PVS是一個(gè)強(qiáng)大的原型證明系統(tǒng)，最大的優(yōu)勢(shì)是它的定理證明器，但與Uppaal相比，建模要復(fù)雜許多。 基于上述原因，本文對(duì)一

4、個(gè)實(shí)時(shí)系統(tǒng)用Uppaal建模，然后將其轉(zhuǎn)化為PVS能接受的格式，再用PVS系統(tǒng)進(jìn)行驗(yàn)證。具體方法是先用PVS建立一個(gè)模板以體現(xiàn)時(shí)間自動(dòng)機(jī)的共性，然后解析Uppaal建模生成的規(guī)格說明以抽取信息來生成PVS時(shí)間自動(dòng)機(jī)模板參數(shù)。模板與參數(shù)一起構(gòu)成了具體的PVS時(shí)間自動(dòng)機(jī)規(guī)格說明。同時(shí)將Uppaal中的特性轉(zhuǎn)換成PVS的證明責(zé)任。其本質(zhì)就是將模型檢查問題轉(zhuǎn)化成為定理證明問題。最大的意義就是充分發(fā)揮了Uppaal建模簡(jiǎn)單和PVS定理證明功能強(qiáng)大