陳少傑臺灣大學:電子工程學研究所陳拓宇Chen, To-YuTo-YuChen2010-07-142018-07-102010-07-142018-07-102008U0001-3007200815393400http://ntur.lib.ntu.edu.tw//handle/246246/189116本文提出非關鍵路徑切割法(non-critical path slicing)來緩和模型驗證(model checking)中狀態空間暴增(state space explosion)的問題。非關鍵路徑切割法是一種組合式的自動機簡化(compositional automata reduction)。本方法藉由刪除特性獨立的狀態轉換，可以在系統狀態圖(system state graph)產生之前減少驗證的狀態空間。相較於影響錐簡化法(cone of influence reduction)，本方法除了考慮變數的相依性，也根據系統特性的語意來決定特性獨立的狀態轉換。本文提供理論上的證明以確保驗證結果的正確性，並應用本文提出之方法於實際的例子。實驗顯示本方法在變數之相依程度很高的情況下，仍可提高模型驗證的執行效果。Model checking is a formal verification method that automatically checks whether a system satisfies its property or not. The system behavior can be modeled by a system state graph, and the model checker will explore the entire system state graph to verify design correctness. However, model checking is limited by the state space explosion problem. Model reduction techniques alleviate this limitation by reducing the model size and preserve sufficient information to verify the system against a given property. In this Thesis, we present a compositional reduction method that reduces the automata model before the system state graph is generated. Reduction is based on the semantics for temporal logic properties of the forms EG(f1) and E(f1 U f2), where f1 and f2 are propositional logics. Non-critical paths which do that affect the property are sliced out through the elimination of property independent transitions. We theoretically justified our reduction method and provided experimental results on several case studies.ABSTRACT iIST OF FIGURES vIST OF TABLES vii. INTRODUCTION 1.1 Model Checking 1.2 Thesis Motivation 1 .3 Thesis Overview 3. RELATED WORK 5.1 Model Abstraction Techniques 5.2 Model Reduction Techniques 6. PRELIMINARIES 9. NON-CRITICAL PATH SLICING 15.1 Overview 17.2 Model Reduction 17.2.1 Property Independent Transitions for EG 18.2.2 Property Independent Transitions for EU 19.2.3 Property Independent Guards and Assignments 21.3 Property Preserving 22.4 Application Example 25.5 Summary 29. EXPERIMENTAL RESULT 31.1 Evaporator System 31.1.1 Results for Evaporator System 32.2 Simple Bus Arbiter System 35.2.1 Results for Simple Bus Arbiter System 35.3 Window Control System 37.3.1 Results for Window Control System 41.4 Traffic Light Controller 42.4.1 Results for Traffic Light Controller 44.5 Summary 45. CONCLUSION AND FUTURE WORK 47IBLIOGRAPHY 49826040 bytesapplication/pdfen-US模型驗證擴充式真時自動機簡化非關鍵路徑切割影響錐model checkingextended timed automatareductionnon-critical pathslicingcone of influencethesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/189116/1/ntu-97-R95943163-1.pdf