PPTL模型檢測器的改進及應用.pdf

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

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