| 摘要 | 第3-6页 |
| ABSTRACT | 第6-8页 |
| CHAPTER 1 INTRODUCTION | 第17-42页 |
| 1.1 RESEARCH BACKGROUND | 第17-18页 |
| 1.2 RESEARCH OBJECTIVE AND CONTENTS | 第18-21页 |
| 1.3 RESEARCH STATUS AND ANALYSIS | 第21-30页 |
| 1.3.1 Study on Code Analysis Technique(Symbolic Execution) | 第22-24页 |
| 1.3.2 Study on Verification Technique(Model Checking) | 第24-27页 |
| 1.3.3 Study on Compilers for Robust Binaries Generation | 第27-28页 |
| 1.3.4 Study on Crash and Bugs on Verified Applications | 第28-29页 |
| 1.3.5 Study on Making USB Hard Disk as an Installation Resource | 第29-30页 |
| 1.4 RESEARCH PROBLEM AND METHODS IMPLEMENTED | 第30-33页 |
| 1.4.1 Optimization of Parallel Code Analysis Tool | 第30-31页 |
| 1.4.2 Improving the Verification Technique | 第31-32页 |
| 1.4.3 Analyzing the Reliable C Compiler for Highly Available Binaries | 第32页 |
| 1.4.4 Developing the Anticrasher Tool to Prevent Crash at User End | 第32-33页 |
| 1.4.5 Making USB HD as Popular OSs Installation Resource | 第33页 |
| 1.5 MAJOR WORK AND ACHIEVEMENTS | 第33-40页 |
| 1.5.1 Major Contributions | 第34-35页 |
| 1.5.2 Detailed Contributions | 第35-40页 |
| 1.6 CHAPTER ORGANIZATION | 第40-41页 |
| 1.7 SUMMARY | 第41-42页 |
| CHAPTER 2 OPTIMIZING CLOUD9 TO ENHANCE CODE ANALYSIS | 第42-79页 |
| 2.1 SYMBOLIC EXECUTION | 第43-46页 |
| 2.1.1 Introduction | 第43-44页 |
| 2.1.2 Background and Limitations | 第44页 |
| 2.1.3 First Breakthrough:Incorporating with Constraint Solver | 第44-45页 |
| 2.1.4 Second Breakthrough:Introducing Layers of Constraint Solvers(KLEE) | 第45页 |
| 2.1.5 Third Breakthrough:Parallel Symbolic Execution Engines | 第45-46页 |
| 2.2 RESEARCH MOTIVATION,RELATED WORK AND CONTRIBUTION | 第46-49页 |
| 2.2.1 Research Motivation | 第46页 |
| 2.2.2 Related Work | 第46-48页 |
| 2.2.3 Our Contributions | 第48-49页 |
| 2.3 FIELD STUDY ON SYMBOLIC EXECUTION TOOLS(KLEE AND CLOUD9) | 第49-57页 |
| 2.3.1 Details of Self-Written Benchmarks | 第49-50页 |
| 2.3.2 Data Collection | 第50-51页 |
| 2.3.3 Execution Time Calculation | 第51页 |
| 2.3.4 Observation and Error Handling | 第51-54页 |
| 2.3.5 Major Findings | 第54-57页 |
| 2.4 TUNING STRATEGIES ON CLOUD | 第57-64页 |
| 2.4.1 Dynamic Worker Synchronization | 第58-59页 |
| 2.4.2 Modify Job Distribution Policy | 第59-61页 |
| 2.4.3 Cache Management of Solved Constraints | 第61-63页 |
| 2.4.4 Discussion on the Tuning Strategy | 第63-64页 |
| 2.5 EVALUATION OF TUNED CLOUD | 第64-74页 |
| 2.5.1 The Improvement over Cloud | 第65-68页 |
| 2.5.2 Effectiveness of Real-World Benchmarks | 第68-73页 |
| 2.5.3 Evaluation Result | 第73-74页 |
| 2.6 SURVEY OF THE THIRD MODIFICATION ON CLOUD | 第74-78页 |
| 2.6.1 Users and Machines Selection | 第74页 |
| 2.6.2 Survey Setup | 第74-75页 |
| 2.6.3 Survey Result | 第75页 |
| 2.6.4 Result Analysis | 第75-78页 |
| 2.6.5 Survey Feedback | 第78页 |
| 2.7 CONCLUSION ON ENHANCING CLOUD | 第78页 |
| 2.8 SUMMARY | 第78-79页 |
| CHAPTER 3 MODEL CHECKING FOR CRASH FREE SOFTWARE | 第79-125页 |
| 3.1 MODEL CHECKING | 第80-83页 |
| 3.1.1 Introduction | 第80-81页 |
| 3.1.2 Background | 第81-82页 |
| 3.1.3 Limitations of Model Checking | 第82-83页 |
| 3.1.4 Breakthroughs | 第83页 |
| 3.2 MOTIVATION AND CONTRIBUTIONS | 第83-84页 |
| 3.3 PAPER SELECTION FOR SURVEY | 第84-92页 |
| 3.3.1 Publications on Model Checking | 第84-87页 |
| 3.3.2 Publications at Reputed Venues | 第87-92页 |
| 3.4 MODEL CHECKING TO VERIFY SOFTWARE APPLICATION | 第92-102页 |
| 3.4.1 Background | 第92-93页 |
| 3.4.2 An Example of Model Checking Process | 第93-95页 |
| 3.4.3 Extending Scalability of Model Checking | 第95-100页 |
| 3.4.4 Verifying Other Software Artefacts | 第100-101页 |
| 3.4.5 Verifying Software Product-Lines | 第101-102页 |
| 3.5 MODEL CHECKING FOR SOFTWARE TESTING AND PROGRAM ANALYSIS | 第102-106页 |
| 3.5.1 Model Checking for Software Testing and Debugging | 第102-104页 |
| 3.5.2 Model Checking and Code Analysis | 第104-106页 |
| 3.6 STATE-EXPLOSION PROBLEM AND SOLUTIONS | 第106-114页 |
| 3.6.1 Problem Description | 第106-107页 |
| 3.6.2 Solutions to State-Explosion | 第107-113页 |
| 3.6.3 Discussions on Existing Solutions | 第113页 |
| 3.6.4 Our Approach | 第113-114页 |
| 3.7 MODEL CHECKING TOOLS | 第114-121页 |
| 3.7.1 Spin | 第114-115页 |
| 3.7.2 Java Path Finder(JPF) | 第115-116页 |
| 3.7.3 Symbolic Model Checkers | 第116页 |
| 3.7.4 Bounded Model Checkers | 第116-117页 |
| 3.7.5 Probabilistic Model Checkers | 第117页 |
| 3.7.6 Dynamic Model Checkers | 第117-118页 |
| 3.7.7 Domain-Specific Model Checkers | 第118页 |
| 3.7.8 Compositional Model Checkers | 第118页 |
| 3.7.9 Combined Model Checkers | 第118-119页 |
| 3.7.10 Other Model Checkers | 第119-121页 |
| 3.8 INTEGRATION WITH OTHER ANALYSIS AND VERIFICATION TECHNIQUES | 第121-123页 |
| 3.8.1 Type System | 第121-122页 |
| 3.8.2 Symbolic Execution | 第122页 |
| 3.8.3 Theorem Proving | 第122-123页 |
| 3.9 CONCLUSION ON MODEL CHECKING FOR CRASH FREE SOFTWARE | 第123-124页 |
| 3.10 SUMMARY | 第124-125页 |
| CHAPTER 4 RELIABLE COMPILER TO GENERATE ROBUST BINARIES | 第125-153页 |
| 4.1 MOTIVATION,RELATED WORK,AND CONTRIBUTION | 第125-127页 |
| 4.1.1 Motivation | 第125-126页 |
| 4.1.2 Related Work | 第126-127页 |
| 4.1.3 Our Contributions | 第127页 |
| 4.2 BASIC IDEA,PROFILE SETUP,AND METHODOLOGY | 第127-133页 |
| 4.2.1 Basic Idea | 第127-130页 |
| 4.2.2 Profile Setup | 第130-131页 |
| 4.2.3 Methodology | 第131-133页 |
| 4.3 PERFORMANCE COMPARISON ON FEDORA OS | 第133-138页 |
| 4.3.1 Comparison of Compilation Time | 第133页 |
| 4.3.2 Comparison of Size of Generated Binaries | 第133页 |
| 4.3.3 Comparison of Dynamic Performance of Generated Binaries | 第133-138页 |
| 4.4 PERFORMANCE COMPARISON ON WINDOWS VISTA(64-BIT) | 第138-142页 |
| 4.4.1 Comparison of Compilation Time | 第138-139页 |
| 4.4.2 Comparison of Size of Generated Binaries | 第139页 |
| 4.4.3 Comparison of Dynamic Performance of Generated Binaries | 第139-142页 |
| 4.5 PERFORMANCE COMPARISON ON MAC OS X | 第142-143页 |
| 4.5.1 Comparison of Compilation Time | 第143页 |
| 4.5.2 Comparison of Size of Generated Binaries | 第143页 |
| 4.6 PERFORMANCE COMPARISON OF INTEL AND PGI ON ALL THREE OSS | 第143-145页 |
| 4.7 RESULT ANALYSIS | 第145-152页 |
| 4.7.1 General Observation | 第145-147页 |
| 4.7.2 Ranking of Compilers on Fedora OS | 第147-149页 |
| 4.7.3 Ranking of Compilers on Windows OS | 第149-150页 |
| 4.7.4 Ranking of Compilers on Mac OS | 第150-151页 |
| 4.7.5 Ranking of Intel and PGI on All OSs | 第151-152页 |
| 4.7.6 Surveying the Results | 第152页 |
| 4.8 CONCLUSION ON RELIABLE COMPILER FOR ROBUST BINARIES GENERATION | 第152页 |
| 4.9 SUMMARY | 第152-153页 |
| CHAPTER 5 ANTICRASHER TOOL TO PREVENT CRASH AT USER END | 第153-168页 |
| 5.1 CASE STUDIES ON CRASH | 第154-157页 |
| 5.1.1 Blue Screen of Death(BSOD) | 第154-155页 |
| 5.1.2 Windows Explorer Crash | 第155页 |
| 5.1.3 Other Application Crash | 第155-156页 |
| 5.1.4 Heavy Memory Consumer | 第156-157页 |
| 5.1.5 Heavy CPU Consumer | 第157页 |
| 5.2 MOTIVATION,RELATED WORK AND CONTRIBUTIONS | 第157-161页 |
| 5.2.1 Motivation | 第157-158页 |
| 5.2.2 Related Work | 第158-161页 |
| 5.2.3 Our Contributions | 第161页 |
| 5.3 BASIC IDEA OF ANTICRASHER TOOL | 第161-164页 |
| 5.3.1 Startup | 第162页 |
| 5.3.2 Checkpoint(CP)Generation | 第162页 |
| 5.3.3 Monitoring | 第162-163页 |
| 5.3.4 Prediction | 第163-164页 |
| 5.3.5 The Development | 第164页 |
| 5.4 EVALUATION OF SIMPLE ANTICRASHER | 第164-167页 |
| 5.4.1 Discussion on the Tool | 第165-167页 |
| 5.5 CONCLUSION ON ANTICRASHER | 第167页 |
| 5.6 SUMMARY | 第167-168页 |
| CHAPTER 6 EXTERNAL USB HARD DISK FOR OSS INSTALLATION | 第168-190页 |
| 6.1 INTRODUCTION | 第169-173页 |
| 6.1.1 Motivation | 第170-172页 |
| 6.1.2 Related Work | 第172页 |
| 6.1.3 Our Contributions | 第172-173页 |
| 6.2 USB-STICK AS A REPLACEMENT | 第173-183页 |
| 6.2.1 Windows OS Installation Resource | 第173-179页 |
| 6.2.2 Ubuntu/Kubuntu/Xubuntu OS Installation Resource | 第179页 |
| 6.2.3 Fedora OS Installation Resource | 第179-181页 |
| 6.2.4 Solaris OS Installation Resource | 第181-182页 |
| 6.2.5 Mac OS x86 Installation Resource | 第182-183页 |
| 6.3 USB HD AS AN INSTALLATION RESOURCE FOR BIOS BOOTABLE SYSTEM | 第183-188页 |
| 6.3.1 Basic Idea | 第184页 |
| 6.3.2 Challenges and Solutions of Basic Idea | 第184页 |
| 6.3.3 Step1:Partitioning the USB Hard Disk | 第184-185页 |
| 6.3.4 Step2:Copying the Installation Resources | 第185-186页 |
| 6.3.5 Step3:Installing the Required Boot Loader for OSs | 第186页 |
| 6.3.6 Step4:Installing Main Boot Loader on USB HD | 第186-187页 |
| 6.3.7 Step5:Editing GRUB Configuration | 第187页 |
| 6.3.8 Final Display | 第187-188页 |
| 6.4 UPDATE WORK FOR BIOS/UEFI BOOTABLE SYSTEM | 第188-189页 |
| 6.5 CONCLUSION ON MULTI-OPERATIVE USB-HD | 第189页 |
| 6.6 SUMMARY | 第189-190页 |
| CHAPTER 7 CONCLUSION | 第190-191页 |
| REFERENCES | 第191-210页 |
| ACKNOWLEDGEMENTS | 第210-211页 |
| ACCEPTED RESEARCH PAPERS DURING PHD | 第211-212页 |
