| 摘要 | 第1-5页 |
| Abstract | 第5-12页 |
| Chapter 1 Introduction | 第12-19页 |
| ·Background | 第12-14页 |
| ·Properties Need to be Checked in Formal Verification | 第14-15页 |
| ·Problems | 第15-16页 |
| ·Proposal | 第16-17页 |
| ·Thesis Outline | 第17-18页 |
| ·Summary | 第18-19页 |
| Chapter 2 Prerequisite Knowledge | 第19-27页 |
| ·Brief Explanation of TLA | 第19-20页 |
| ·Propositional Logic | 第20-22页 |
| ·Set Theory | 第22-24页 |
| ·Predicate Logic | 第24页 |
| ·Linear Temporal Logic | 第24-26页 |
| ·Summary | 第26-27页 |
| Chapter 3 Divide and Conquer Paradigm for System Specification Refinement | 第27-33页 |
| ·Brief Explanation of Divide and Conquer Paradigm | 第27页 |
| ·Module State Machine for Representation of Specification | 第27-29页 |
| ·Detailed Steps of Using D&C Paradigm for Specification Refinement | 第29-32页 |
| ·Summary | 第32-33页 |
| Chapter 4 System Specification Refinement | 第33-58页 |
| ·Concise System Specification | 第33-38页 |
| ·Telegram Structure | 第34-35页 |
| ·Communication Schema | 第35页 |
| ·Timing Restrictions | 第35-36页 |
| ·System States and Behaviors | 第36-38页 |
| ·Mutual Checking between MPU’s | 第38页 |
| ·System Division | 第38-49页 |
| ·System Overall Hierarchical Break-down Structure | 第38-39页 |
| ·First Level Division | 第39-40页 |
| ·Second Level Division | 第40-47页 |
| ·Third Level Division | 第47-49页 |
| ·System Conquest | 第49-56页 |
| ·Robot Refinement | 第49页 |
| ·Mutual Checking Refinement | 第49-50页 |
| ·SM_WHT Refinement | 第50-53页 |
| ·SM_HC Refinement | 第53-54页 |
| ·Module Integration | 第54-56页 |
| ·Liveness and Fairness Properties Analysis | 第56页 |
| ·Summary | 第56-58页 |
| Chapter 5 Implementation of Models in TLA | 第58-77页 |
| ·Implementation of Telegram Model | 第58-60页 |
| ·Implementation of MPU Model | 第60-61页 |
| ·Implementation of HC Model | 第61-67页 |
| ·Modeling Telegram Sending Logic | 第61-63页 |
| ·Modeling Telegram Receiving Logic | 第63-67页 |
| ·Implementation of WHT Model | 第67-72页 |
| ·Implementation of Mutual Checking Function | 第72-73页 |
| ·Implementation of Communication Channel Model | 第73-76页 |
| ·Implementation of Liveness and Fairness Property | 第76页 |
| ·Summary | 第76-77页 |
| Chapter 6 Model Analysis | 第77-82页 |
| ·Verification Result of the System Model | 第77-78页 |
| ·Limitations of TLA and its Model Checker TLC | 第78-81页 |
| ·State Explosion Problem | 第79-80页 |
| ·Stuttering Steps | 第80-81页 |
| ·Summary | 第81-82页 |
| Conclusion | 第82-84页 |
| References | 第84-88页 |
| Appendix | 第88-103页 |
| Extended Abstract in Chinese | 第103-107页 |
| Acknowledgement | 第107-108页 |
| Resume | 第108-109页 |
