PPTL模型檢測器的改進(jìn)及應(yīng)用.pdf

1、模型檢測是一種形式化驗(yàn)證方法，目前已經(jīng)得到了廣泛的發(fā)展和應(yīng)用。本文給出的是一種基于命題投影時(shí)序邏輯(Propositional Projection Temporal Logic，PPTL)的模型檢測器的改進(jìn)和應(yīng)用，該模型檢測器是在SPIN的基礎(chǔ)上添加和修改部分模塊實(shí)現(xiàn)的。PPTL模型檢測器用Promela語言描述系統(tǒng)模型，用PPTL公式描述待驗(yàn)證的系統(tǒng)性質(zhì)。由于PPTL在SPIN中無法識(shí)別，因此需要將PPTL公式轉(zhuǎn)換為SPIN可接收的

2、Never Claim，才能夠在SPIN基礎(chǔ)之上實(shí)現(xiàn)PPTL模型檢測。
　　本文主要研究PPTL公式到Never Claim的改進(jìn)轉(zhuǎn)換算法。首先，簡單介紹了PPTL的語法、語義以及一些等價(jià)關(guān)系和邏輯法則等，還給出了模型檢測技術(shù)的原理和發(fā)展，并重點(diǎn)介紹了模型檢測器SPIN的相關(guān)內(nèi)容，然后詳細(xì)介紹了PPTL公式向Never Claim轉(zhuǎn)換的過程：PFTL公式→范式(Normal Form，NF)→帶標(biāo)記的范式圖(Labeled Nor