Uppaal時間自動機規(guī)格說明到PVS時間自動機模板的轉換.pdf

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

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

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

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