基于自動機的時間系統(tǒng)形式驗證技術.pdf

1、時間系統(tǒng)的形式驗證因時間域的引入而使研究工作更具挑戰(zhàn)性，越來越受到學術界和工業(yè)界的關注。由于模型檢查技術受狀態(tài)空間等方面的限制，本文以定理證明器’PVS(Prototype Veilfication System)為第三方工具，以時間自動機TA(Timed Automata)理論為基礎，設計開發(fā)了一個能夠進行時間系統(tǒng)形式建模和形式驗證的集成化的形式驗證框架FVofTA(Formal Verification of TlmedAutoma

2、ta)。本文研究工作的創(chuàng)新點主要體現(xiàn)在以下幾個方面： (1) 時間(或時鐘)是描述時間系統(tǒng)的必備要素，我們用PVS形式化了用于對時間系統(tǒng)形式建模的時間(時鐘)理論。這是建模時間系統(tǒng)的基礎，同時為了方便和簡化建模過程，給出了一些格式化的共有操作。 (2) 在(1)的基礎上用PVS規(guī)格說明語言實現(xiàn)了時間自動機的語法和語義理論，并形式化了關于時間自動機的許多有關性質(zhì)，為時間系統(tǒng)有關性質(zhì)的形式驗證作了必要的準備工作。 (

3、3) 根據(jù)時間自動機的語法元素的特征和關于操作自動機的某些方法，抽象出了在FVofTA中對一般時間系統(tǒng)進行形式建模的模板，以及根據(jù)子自動機間的通訊方式求取積自動機的模板，利用這些模板，可高效方便地對一般的時間系統(tǒng)建模。 (4) 在FVofTA中建立了時間化的時序邏輯形式體系，該體系基于時間自動機語義，既可以用來描述安全性，也可以用來描述有界活性，為時間系統(tǒng)性質(zhì)的規(guī)格說明提供了一致的描述接口。 (5) 以(2)中的規(guī)格說明

4、為基礎，建立了關于時間系統(tǒng)狀態(tài)不變性(也稱為安全性)的形式驗證框架。利用(2)中形成的關于時間自動機運行的特點，根據(jù)不變式是歸納的這一特點，可以使用相對統(tǒng)一的證明過程來證明安全性。 (6) 開發(fā)了一系列用于提高形式驗證效率的證明策略。 (7) 為了考察系統(tǒng)的整個可達狀態(tài)空間，基于區(qū)域等價理論，在FVofTA中集成了部分模型檢查算法，可以使用狀態(tài)有窮性這一特征來判斷某個時間系統(tǒng)的時間行為中是否含有死鎖，判斷某一狀態(tài)是否初態(tài)