基于自動(dòng)機(jī)的時(shí)間系統(tǒng)形式驗(yàn)證技術(shù).pdf

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

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

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

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