| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| LIST OF ABBREVIATIONS | 第13-17页 |
| Chapter 1 Introduction | 第17-29页 |
| 1.1 Formal Verification Techniques | 第17-23页 |
| 1.1.1 Theorem Proving | 第18-19页 |
| 1.1.2 Model Checking | 第19-23页 |
| 1.2 Temporal Logic | 第23-25页 |
| 1.3 Contributions | 第25-27页 |
| 1.4 Dissertation Organization | 第27-29页 |
| Chapter 2 Propositional Projection Temporal Logic | 第29-37页 |
| 2.1 Syntax and Semantics | 第29-31页 |
| 2.2 Derived Formulas and Logical Laws | 第31-32页 |
| 2.2.1 Derived Formulas | 第31页 |
| 2.2.2 Logical Laws | 第31-32页 |
| 2.3 Satisfaction, Validity and Precedence Rules | 第32-33页 |
| 2.4 Normal Form and Labeled Normal Form Graph | 第33-36页 |
| 2.4.1 Normal Form | 第33-35页 |
| 2.4.2 Labeled Normal Form Graph | 第35-36页 |
| 2.5 Summary | 第36-37页 |
| Chapter 3 Symbolic Representation of System Models | 第37-51页 |
| 3.1 Binary Decision Diagram | 第37-41页 |
| 3.2 Ordering and Reducing | 第41-43页 |
| 3.3 Kripke Structure | 第43-44页 |
| 3.4 Encoding of States | 第44-45页 |
| 3.5 Representing Sets of States | 第45-47页 |
| 3.6 Representing Sets of State Transitions | 第47-48页 |
| 3.7 Representing Labeling Function | 第48-49页 |
| 3.8 Summary | 第49-51页 |
| Chapter 4 Symbolic Model Checking of PPTL | 第51-79页 |
| 4.1 Explicit model checking of PPTL | 第51-52页 |
| 4.2 Set of satisfying states | 第52-56页 |
| 4.3 Symbolic model checking of PPTL Specifications | 第56-59页 |
| 4.4 Complexity of Symbolic PPTL Model Checking | 第59-65页 |
| 4.5 Case studies | 第65-78页 |
| 4.5.1 A Case Study — Verilog HDL Program | 第65-72页 |
| 4.5.2 A Case Study — Railroad Crossing Control System | 第72-78页 |
| 4.6 Summary | 第78-79页 |
| Chapter 5 Formal Verification of Real Time Systems | 第79-93页 |
| 5.1 Background | 第79-80页 |
| 5.2 Verification of Rate Monotonic Scheduling Algorithm | 第80-86页 |
| 5.2.1 Rate Monotonic Scheduling Algorithm | 第80-82页 |
| 5.2.2 Modeling and Verification of RMS Algorithm | 第82-86页 |
| 5.3 Verification of Delayed Rate Monotonic Scheduling Algorithm | 第86-92页 |
| 5.3.1 Delayed Rate Monotonic Scheduling Algorithm | 第86-88页 |
| 5.3.2 Modeling and Verification of DRMS Algorithm | 第88-92页 |
| 5.4 Summary | 第92-93页 |
| Chapter 6 PPTL Symbolic Model Checker | 第93-109页 |
| 6.1 NuSMV Model Checker | 第94-98页 |
| 6.2 PLSMC — A PPTL Symbolic Model Checker | 第98-102页 |
| 6.2.1 Design of PLSMC | 第98-100页 |
| 6.2.2 Implementation of PLSMC | 第100-102页 |
| 6.3 Experimental Results | 第102-106页 |
| 6.3.1 Gigamax Cache Consistency Protocol | 第102-103页 |
| 6.3.2 Alternating Bit Protocol | 第103-105页 |
| 6.3.3 PCI Bus Protocol | 第105-106页 |
| 6.4 Summary | 第106-109页 |
| Chapter 7 Conclusions and Future Works | 第109-113页 |
| 7.1 Conclusions | 第109-110页 |
| 7.2 Future Works | 第110-113页 |
| ACKNOWLEDGEMENTS | 第113-115页 |
| REFERENCES | 第115-123页 |
| BIOGRAPHY | 第123-124页 |
