| 作者简介 | 第1-4页 |
| 摘要 | 第4-5页 |
| Abstract | 第5-10页 |
| 1 Introduction | 第10-18页 |
| ·Formal Methods | 第10-13页 |
| ·Formal Specification | 第11-12页 |
| ·Formal Verification | 第12-13页 |
| ·Model Checking | 第12-13页 |
| ·Theorem Proving | 第13页 |
| ·Temporal Logic and Temporal Logic Programming | 第13-16页 |
| ·Temporal Logic | 第13-15页 |
| ·Temporal Logic Programming | 第15-16页 |
| ·Contributions | 第16-17页 |
| ·The Organization of the Thesis | 第17-18页 |
| 2 Propositional Projection Temporal Logic | 第18-28页 |
| ·Syntax and Semantics | 第18-22页 |
| ·Syntax | 第18页 |
| ·Semantics | 第18-22页 |
| ·Precedence Rules and Properties of Formulas | 第22页 |
| ·Precedence Rules | 第22页 |
| ·Properties of Formulas | 第22页 |
| ·Discussion | 第22-24页 |
| ·Similarities | 第23页 |
| ·Specific Characteristics | 第23-24页 |
| ·Derived Formulas and Logical Laws | 第24-26页 |
| ·Derived Formulas | 第24-25页 |
| ·Logical Laws | 第25-26页 |
| ·Conclusion | 第26-28页 |
| 3 The Proof System for Propositional Projection Temporal Logic | 第28-54页 |
| ·Proof System | 第28-32页 |
| ·Axioms | 第28-31页 |
| ·Inference Rules | 第31-32页 |
| ·Formal Proof and Theorems | 第32页 |
| ·Soundness | 第32-38页 |
| ·Completeness | 第38-49页 |
| ·A Case Study — Mutual Exclusion | 第49-52页 |
| ·Conclusion | 第52-54页 |
| 4 Cylinder Computation Model | 第54-78页 |
| ·Projection Temporal Logic | 第55-58页 |
| ·Syntax | 第55-56页 |
| ·Semantics | 第56-58页 |
| ·Modeling, Simulation and Verification Language | 第58-60页 |
| ·Framing | 第58-59页 |
| ·Expressions and Statements | 第59-60页 |
| ·Normal Form of MSVL | 第60页 |
| ·Sequence Expression | 第60-63页 |
| ·CCM | 第63-66页 |
| ·Operational Semantics | 第66-70页 |
| ·Operational Semantics of MSVL | 第66-67页 |
| ·Operational Semantics of CCM | 第67-70页 |
| ·Implementation of CCM in MSVL | 第70-73页 |
| ·MSVL Interpreter | 第70-71页 |
| ·Implementation of CCM | 第71-73页 |
| ·Reduction of Parallel | 第72页 |
| ·Reduction of Over | 第72-73页 |
| ·A Case Study — Word Processor | 第73-76页 |
| ·Conclusion | 第76-78页 |
| 5 Formal Verification of Real Time Systems | 第78-104页 |
| ·Deadline Driven Scheduler | 第78-79页 |
| ·Formalization of the Deadline Driven Scheduler | 第79-81页 |
| ·Proof of Liu and Layland’s Theorem | 第81-103页 |
| ·Formal Proof of Theorems | 第81-86页 |
| ·Lemmas | 第86-101页 |
| ·Sufficiency | 第101-102页 |
| ·Necessity | 第102-103页 |
| ·Conclusion | 第103-104页 |
| 6 Formal Verification of Hardware Designs | 第104-118页 |
| ·Verification of the Full Adder | 第104-109页 |
| ·Full Adder | 第104-105页 |
| ·Modeling and Verification of the Full Adder | 第105-109页 |
| ·Formal Verification of Carry Lookahead Adder | 第109-116页 |
| ·Carry Lookahead Adder | 第109-112页 |
| ·Modeling and Verification of the Carry Lookahead Adder | 第112-116页 |
| ·Conclusion | 第116-118页 |
| 7 Conclusions and Future Works | 第118-120页 |
| ·Conclusions | 第118-119页 |
| ·Future Works | 第119-120页 |
| Acknowledgements | 第120-122页 |
| References | 第122-130页 |
| Finished Papers | 第130-131页 |
