| 1. Introduction | 第1-11页 |
| 2. Alloy | 第11-20页 |
| ·Language | 第11-17页 |
| ·Expressions | 第11-12页 |
| ·Formulas | 第12-14页 |
| ·High-Level Constructs | 第14-17页 |
| ·Ordering Relations | 第17-18页 |
| ·Analyzer | 第18-20页 |
| 3. UML | 第20-27页 |
| ·What is UML? | 第20页 |
| ·Why Use UML? | 第20页 |
| ·Types of UML Diagrams | 第20-27页 |
| ·UML Diagrams | 第20-24页 |
| ·Use Case Diagrams | 第21-22页 |
| ·Class Diagrams | 第22-23页 |
| ·Interaction Diagrams | 第23页 |
| ·Collaboration diagrams: | 第23页 |
| ·State Diagrams | 第23-24页 |
| ·Activity Diagrams | 第24页 |
| ·Physical Diagrams | 第24页 |
| ·Extended of UML Diagrams | 第24-27页 |
| 4 Requirements modeling | 第27-37页 |
| ·Library System introduction | 第27页 |
| ·Model objects of the system | 第27-31页 |
| ·Classes and associations | 第27-29页 |
| ·System state | 第29-31页 |
| ·Mode the facts and invariants | 第31-33页 |
| ·Facts | 第31-32页 |
| ·Business policies (Invariants) | 第32-33页 |
| ·Model the operation | 第33-37页 |
| ·Borrow a book | 第33-35页 |
| ·Return book | 第35-37页 |
| 5. Transforming Requirement to Design | 第37-69页 |
| ·Step down to Sequential Operations Model | 第38-50页 |
| ·Break down the operation process | 第39-40页 |
| ·Example runs | 第40-41页 |
| ·Verify the correctness. | 第41-50页 |
| ·Evolve to Relational Data Model | 第50-58页 |
| ·Change Objects Declarations to Relational Data Model | 第51-56页 |
| ·Add ID to every object | 第51-52页 |
| ·Transform Objects relations | 第52-53页 |
| ·Leave global states unchanged | 第53页 |
| ·Transform operations on object. | 第53-56页 |
| ·Transform run results | 第56页 |
| ·Verify the correctness | 第56-58页 |
| ·Introduce multithreads and apply looks | 第58-69页 |
| ·Transformation | 第58-65页 |
| ·Slice states and multithreads preparation | 第59-60页 |
| ·Mutex and its operations | 第60-61页 |
| ·Deadlock detection | 第61-63页 |
| ·Utilize lock to operations | 第63-65页 |
| ·Example runs | 第65-66页 |
| ·Verify the correctness | 第66-69页 |
| 6. Conclusion, future work and Related work | 第69-70页 |
| ·Conclusion, future work | 第69页 |
| ·Related work | 第69-70页 |
| Bibliography | 第70-71页 |
