| 中文摘要 | 第3-5页 |
| ABSTRACT | 第5-6页 |
| CHAPTER 1 INTRODUCTION | 第14-22页 |
| 1.1 BACKGROUND OF RESEARCH | 第14-16页 |
| 1.2 Current Status of research | 第16-18页 |
| 1.3 RESEARCH OBJECTIVES | 第18-19页 |
| 1.4 OUTLINE | 第19-22页 |
| CHAPTER 2 THEORETICAL AND TECHNICAL FOUNDATIONS | 第22-56页 |
| 2.1 THE OMG APPROACH AND TERMINOLOGY | 第22-34页 |
| 2.1.1 Model- Driven Engineering (MDE) | 第22页 |
| 2.1.2 Model-driven development (MDD) | 第22-23页 |
| 2.1.3 Model-Driven Architecture (MDA) | 第23-26页 |
| 2.1.4 Model Transformation | 第26-28页 |
| 2.1.5 Model Transformations Languages | 第28-29页 |
| 2.1.6 Unified Modelling Language (UML) | 第29-34页 |
| 2.2 FORMAL VERIFICATION TECHNIQUES | 第34页 |
| 2.3 MODEL CHECKING | 第34-37页 |
| 2.3.1 Advantages and disadvantages of model checking | 第36页 |
| 2.3.2 Verification tools | 第36-37页 |
| 2.4 FORMAL METHODS | 第37-42页 |
| 2.4.1 Applying Formal Methods | 第38-39页 |
| 2.4.2 Advantages of Applying Formal Methods | 第39页 |
| 2.4.3 Classification of Formal Methods | 第39页 |
| 2.4.4 Overview of Some Formal Methods | 第39-42页 |
| 2.5 COLOURED PETRI NETS (CPN) MODELING | 第42-45页 |
| 2.5.1 Advantages of Coloured Petri Nets | 第43-44页 |
| 2.5.2 CPN ML Programming | 第44-45页 |
| 2.6 COLOURED PETRI NETS TOOL SUPPORT | 第45-53页 |
| 2.6.1 CPN-Tools | 第45-49页 |
| 2.6.3 Process mining techniques | 第49-53页 |
| 2.7 SUMMARY | 第53-56页 |
| CHAPTER 3 TRANSFORMATIONAL UML 2.0 MODEL | 第56-74页 |
| 3.1 PROPOSED METHODOLOGY | 第56页 |
| 3.2 PRELIMINARIES | 第56-58页 |
| 3.3 ALGORITHM FOR TRANSFORMATION OF UML TO CPN MODEL | 第58-68页 |
| 3.3.1 Mapping use case diagram to CPN model | 第58-61页 |
| 3.3.2 Mapping of Activity diagrams Elements to CPN | 第61-65页 |
| 3.3.3 Translation Rules | 第65-66页 |
| 3.3.4 Algorithms Workflow UML Models to CPN | 第66页 |
| 3.3.5 Proposal of a methodology to CPN model | 第66-67页 |
| 3.3.6 Recommendations to create CPN model | 第67-68页 |
| 3.4 MAPPING CPN MODEL TO MXML | 第68-69页 |
| 3.5 TRANSFORMATION RULES MXML TO CPN | 第69-70页 |
| 3.6 PROCESS MINING ALGORITHMs | 第70-72页 |
| 3.6.1 Alpha++ algorithm | 第70-71页 |
| 3.6.2 Heuristic Miner | 第71-72页 |
| 3.7 SUMMARY | 第72-74页 |
| CHAPTER 4 MODEL VALIDATION AND VERIFICATION | 第74-108页 |
| 4.1 CASE STUDY | 第74-76页 |
| 4.2 SIMULATION | 第76-80页 |
| 4.3 THE PERFORMANCE ANALYSIS MODEL | 第80-82页 |
| 4.4 STATE SPACE GENERATION | 第82-86页 |
| 4.5 GENERIC PROPERTY VERIFICATION | 第86-88页 |
| 4.6 VALIDATION OF THE CPN MODEL | 第88-92页 |
| 4.7 CTL PROPERTIES VALIDATION | 第92-97页 |
| 4.8 PROCESS SIMULATION PROM | 第97-100页 |
| 4.9 PROCESS MINING TECHNIQUES RESULTS | 第100页 |
| 4.10 EXTRACTING INFORMATION FROM LOG FILE | 第100-106页 |
| 4.11 SUMMARY | 第106-108页 |
| CHAPTER 5 CONCLUSION | 第108-110页 |
| 5.1 CONCLUSION | 第108-109页 |
| 5.2 FUTURE WORK | 第109-110页 |
| ACKNOWLEDGEMENTS | 第110-112页 |
| REFERENCES | 第112-122页 |
| GLOSSARY OF TERMS | 第122-124页 |
| APPENDIX 1 | 第124-126页 |
| APPENDIX 2 | 第126-130页 |
| APPENDIX 3 | 第130-136页 |
| APPENDIX 4 | 第136-148页 |
