Formal Schedulability analysis of hierarchical real-time system
- 주제(키워드) Schedulability analysis , Formal methods , UPPAAL
- 발행기관 고려대학교 대학원
- 지도교수 최진영
- 발행년도 2016
- 학위수여년월 2016. 8
- 학위구분 박사
- 학과 대학원 모바일솔루션학과
- 원문페이지 108 p
- 실제URI http://www.dcollection.net/handler/korea/000000068499
- 본문언어 영어
- 제출원본 000045881477
초록/요약
The use of virtualization technology is increasing as it provides many useful features such as efficient use of hardware, easy system migration, and isolation between virtual spaces, which prevents errors affecting each other. Recent development in hardware has made it possible to use operating system virtualization in embedded systems. However, to implement virtualization we need to layer multiple schedulers in a system, which makes it difficult to analyze the system’s schedulability and makes it easy to produce errors such as deadline miss. Errors in safety-critical embedded systems can cause severe damage to life and property. Thus, we must verify the schedulability of hierarchical real-time systems. Analyzing the schedulability of hierarchical real-time systems is difficult because of the systems’ complex behavior. When we include shared resources or dependencies among tasks, schedulability analysis becomes even more complicated. This thesis introduces a framework based on UPPAAL [1] that analyzes the schedulability of hierarchical real-time systems. The framework is first introduced for hierarchical single-core systems and then extended for hierarchical multi-core systems. The extended framework targets several legacy systems on a hierarchical system so that it can process them on a processor efficiently. The basic framework and the extended framework can both specify shared resources and dependencies among tasks as input without additional methods. The framework introduced in this thesis provides several advantages. First, the entire hierarchical real-time system can be formally specified, and the schedulability of the specified system can be formally analyzed without dividing the system. Second, the framework also allows specifying and verifying information on shared resources and dependencies, which makes it possible to detect problems such as priority inversion. Third, the framework counts the preemption events of each task, which helps to update the execution time of each task and provides more accurate schedulability analysis results. Forth, user-defined scheduling policies specified as a UPPAAL timed automata model can be included in the framework. Fifth, the framework can be extended to analyze hierarchical real-time systems that are running on a multi-core platform.
more목차
1. Introduction 1
1.1 Related work 3
1.1.1 Schedulability analysis of two-level hierarchy systems 3
1.1.2 Compositional schedulability analysis 4
1.2 Contribution of this thesis 7
2. Formal Specification and Verification of UPPAAL 12
2.1 Timed automaton in UPPAAL 13
2.1.1 Locations 13
2.1.2 Edges 15
2.2 TCTL 17
3. Schedulability analysis of hierarchical real-time system 18
3.1 Scope 19
3.2 Hierarchical Real-Time System 20
3.3 Framework for Schedulability Analysis of Hierarchical Real-Time System 22
3.4 Resource Request and Allocation Procedure for the Proposed Framework 25
3.5 Preemption Counting 29
3.6 Synchronization among models in the framework 32
3.7 Timed automata models of the framework 36
3.7.1 Resource model of P 36
3.7.2 Resource model of V 38
3.7.3 Model of T 40
4. Extended framework for multi-core 42
4.1 Overview of extended framework 42
4.2 Synchronization of the extended framework 44
4.3 Resource manager model and core model 46
5. Case Study 49
5.1 Verification 49
5.2 Hierarchical systems on a single core 50
5.2.1 An example of a hierarchical system 50
5.2.2 ARINC 653 Avionic systems 54
5.3 Hierarchical multi-core systems 58
6. Conclusion 60
Appendix A. Framework for a single core 62
1. Global declarations 62
1.1 Declarations 63
1.2 System declaration 66
2. Declaration of resource model of P 67
3. Declaration of resource model of V 69
4. Declaration of task model 72
5. Scheduling policies 74
5.1 Model and declaration of earliest deadline first(EDF) 74
5.2 Model and declaration of rate monotonic 76
Appendix B. Framework for multi-core 78
1. Global declarations 78
1.1 Declarations 78
1.2 System declarations 82
2. Declaration of physical resource 83
2.1 Declaration of resource manager model of P 83
2.2 Declaration of core model of P 85
2.3 Model of virtual resource 88
Bibliography 89
