【摘要】：在模型檢驗中,抽象是解決狀態(tài)空間爆炸問題的重要方法.通常的抽象是非強保留的,即可能存在時序性質在抽象模型不滿足而在具體模型滿足的情況.文中首先系統(tǒng)地構造μ-演算Lμ語義模型的安全抽象,在此基礎上,轉換為通用Kripke結構下的安全抽象.然后基于抽象解釋框架及完備抽象解釋和性質強保留之間的關系,構造使得Lμ性質強保留的最小抽象模型精化,并轉換為抽象解釋中抽象域的最小完備精化.依據(jù)此完備抽象域求得性質強保留的最優(yōu)抽象狀態(tài)劃分,從而構造出性質強保留且最優(yōu)的抽象狀態(tài)轉換系統(tǒng).
[Abstract]:Abstraction is an important method to solve the state space explosion problem in model checking. The usual abstraction is not strongly reserved, that is, there may be temporal properties that are not satisfied in the abstract model but satisfied in the concrete model. In this paper, the security abstraction of 渭-calculus L 渭 semantic model is constructed systematically, and on this basis, it is transformed into security abstraction under general Kripke structure. Then, based on the abstract interpretation framework and the relationship between complete abstract interpretation and strong retention of properties, the minimum abstract model with strong retention of L 渭 property is constructed and transformed into the minimum complete refinement of extraction domain in abstract interpretation. According to this complete abstract domain, the optimal abstract state partition with strong property retention is obtained, and the abstract state transition system with strong property retention and optimal property is constructed.
【作者單位】： 武漢大學軟件工程國家重點實驗室;桂林電子科技大學廣西可信軟件重點實驗室;
【基金】：國家自然科學基金(61063002,61100186,61262008) 中國博士后基金(20090450211) 廣西自然科學基金(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220) 武漢大學軟件工程國家重點實驗室開放基金(SKLSE2010-08-06) 廣西壯族自治區(qū)教育廳重點項目基金資助~~
【分類號】：TP306

【相似文獻】

相關碩士學位論文 前1條

1 國瑩;基于共享總線的多核實時系統(tǒng)WCET分析[D];東北大學;2010年

，

本文編號：2478312