| 摘要 | 第6-8页 |
| Abstract | 第8-9页 |
| Resume | 第10-12页 |
| Acknowledgements | 第12-18页 |
| Chapter 1 Introduction | 第18-40页 |
| 1.1 Motivation and Challenges | 第19-23页 |
| 1.2 Research Approach | 第23-24页 |
| 1.3 Research Contributions | 第24-27页 |
| 1.4 Technical Background | 第27-35页 |
| 1.4.1 Logical Clocks | 第27-28页 |
| 1.4.2 CCSL | 第28-30页 |
| 1.4.3 TimeSquare Tool | 第30-31页 |
| 1.4.4 pNets Model | 第31-35页 |
| 1.5 Use Case | 第35-37页 |
| 1.5.1 Vehicle-to-Infrustructure Communications | 第35-36页 |
| 1.5.2 Vehicle-to-Vehicle Communications | 第36-37页 |
| 1.6 The Outline of The Thesis | 第37-40页 |
| Chapter 2 Related Work | 第40-60页 |
| 2.1 Discrete-event Models | 第41-43页 |
| 2.2 Synchronous and Asynchronous Communication Models | 第43-45页 |
| 2.3 BIP Framework | 第45-47页 |
| 2.4 Timed-automata | 第47-49页 |
| 2.5 Timed Petri Nets | 第49-52页 |
| 2.6 AADL | 第52-54页 |
| 2.7 MARTE | 第54-57页 |
| 2.8 STeC | 第57-58页 |
| 2.9 Conclusion | 第58-60页 |
| Chapter 3 pNets With Timed-Actions and LogicalConstraints | 第60-70页 |
| 3.1 Model Building | 第61-64页 |
| 3.1.1 Timed Actions | 第61页 |
| 3.1.2 Logical Constraints | 第61-62页 |
| 3.1.3 Introduce Logical Clocks into pNets Model | 第62-64页 |
| 3.2 Simulation | 第64-68页 |
| 3.2.1 Formalisation of the Architecture | 第65-67页 |
| 3.2.2 Result | 第67-68页 |
| 3.3 Conclusion | 第68-70页 |
| Chapter 4 Timed-pNets Model | 第70-114页 |
| 4.1 Context and problematic | 第71-72页 |
| 4.2 Timed Specification | 第72-79页 |
| 4.2.1 Syntax and Semantic of Clock Relations | 第75-76页 |
| 4.2.2 Properties of the logical clock relations | 第76-79页 |
| 4.3 Timed-pLTS | 第79-81页 |
| 4.4 Timed-pNets | 第81-88页 |
| 4.5 Generating Timed Specification | 第88-104页 |
| 4.5.1 Generating TS of timed-pLTS | 第88-89页 |
| 4.5.2 Auxiliary functions:Pre/Post sets | 第89-90页 |
| 4.5.3 Relations and assignment rules | 第90-92页 |
| 4.5.4 The Method for Generating Timed Specification | 第92-98页 |
| 4.5.5 Generating TS of timed-pNets | 第98-104页 |
| 4.6 Compatibility | 第104-107页 |
| 4.7 Assembling multi-layer timed-pNets system | 第107-108页 |
| 4.8 Simulation | 第108-111页 |
| 4.8.1 Simulation 1 | 第109-110页 |
| 4.8.2 Simulation 2 | 第110-111页 |
| 4.9 Conclusion | 第111-114页 |
| Chapter 5 Delay in Timed-pNets | 第114-134页 |
| 5.1 Context and problematic | 第115-117页 |
| 5.2 Virtual TimeStamps | 第117-119页 |
| 5.3 Time Constraint Conflicts | 第119页 |
| 5.4 Calculate Delays and Delay Bounds | 第119-127页 |
| 5.4.1 Causal Clocks and Causality Paths | 第120-121页 |
| 5.4.2 Computing Delays of clocks | 第121-122页 |
| 5.4.3 Computing Delay Bounds of Clocks | 第122-127页 |
| 5.5 Simulation | 第127-133页 |
| 5.5.1 Encode Properties into TimeSquare | 第128-129页 |
| 5.5.2 Property Checking | 第129-132页 |
| 5.5.3 Discussion | 第132-133页 |
| 5.6 Conclusion | 第133-134页 |
| Chapter 6 Extension of Timed-pNets | 第134-156页 |
| 6.1 Context and problematic | 第135-136页 |
| 6.2 Clock Partition | 第136-148页 |
| 6.2.1 Semantics of Precedence Relations on Partition Clocks | 第138-140页 |
| 6.2.2 Semantics of Coincidence Relations on Partition Clocks | 第140-145页 |
| 6.2.3 Partition Clock Property | 第145-148页 |
| 6.3 Clock Union | 第148-150页 |
| 6.4 Examples and Simulations | 第150-155页 |
| 6.4.1 The Timed Specification of "Control" Component | 第151页 |
| 6.4.2 Timed Specification of "Initial" Component | 第151-152页 |
| 6.4.3 Simulate the "Control" component | 第152-154页 |
| 6.4.4 Simulate the "Initial" component | 第154-155页 |
| 6.5 Conclusion | 第155-156页 |
| Chapter 7 Full Use Case | 第156-178页 |
| 7.1 Use Case | 第157-160页 |
| 7.1.1 Background of ITS | 第157-158页 |
| 7.1.2 Car Inserting Use Case Scenario | 第158-159页 |
| 7.1.3 Properties | 第159-160页 |
| 7.2 Build Timed-pNets Model | 第160-163页 |
| 7.2.1 System Structure | 第160-162页 |
| 7.2.2 Fill Holes | 第162-163页 |
| 7.3 Simulation | 第163-173页 |
| 7.3.1 Simulate the leaf level | 第165-166页 |
| 7.3.2 Simulate the middle level | 第166-171页 |
| 7.3.3 Simulate the top level | 第171-173页 |
| 7.4 Other Simulations | 第173-175页 |
| 7.4.1 Caro communicates with m cars(m>2) | 第173-175页 |
| 7.5 Conclusion | 第175-178页 |
| Chapter 8 Conclusion | 第178-184页 |
| 8.1 Summary and Conclusions | 第179-180页 |
| 8.2 Future Work | 第180-184页 |
| Chapter 9 附录：论文综述（中文版） | 第184-190页 |
| References | 第190-202页 |
| List of publications | 第202-204页 |
| List of Projects Participated | 第204-206页 |
| list of figures | 第206-210页 |
| list of tables | 第210页 |
