Formal Verification and Schedulability Analysis for Hierarchical Real-Time Systems
- 주제(키워드) Hierarchical Real-Time Systems , Formal Methods , Schedulability , Model Checking
- 발행기관 고려대학교 대학원
- 지도교수 최진영
- 발행년도 2012
- 학위수여년월 2012. 8
- 학위구분 박사
- 학과 일반대학원 컴퓨터학과
- 원문페이지 119 p
- 실제URI http://www.dcollection.net/handler/korea/000000035602
- 본문언어 영어
- 제출원본 000045721507
초록/요약
Real-time embedded systems have increased in complexity. As microprocessors become more powerful, the software complexity of real-time embedded systems has been increasing steadily. The requirements for increased functionality and adaptability make the development of real-time embedded software complex and error-prone. Component-based design has been widely accepted as a compositional approach to facilitate the design of complex systems. It provides a means for decomposing a complex system into simpler subsystems and composing the subsystems in a hierarchical manner. A system composed by real-time subsystems with hierarchy is called hierarchical real-time system. Formal methods for real-time systems are mathematically rigorous ways to specify real-time systems and verify real-time properties of the systems. The \textit{Algebra of Communicating Shared Resources with Value Passing} (ACSR-VP) is a process algebraic approach to the formal specification and verification of real-time systems. When applying ACSR-VP to hierarchical real-time systems, there were several issues such as (1) model checking of real-time properties of ACSR-VP models, (2) symbolic deadlock checking of large ACSR-VP specifications and (3) schedulability analysis of hierarchical real-time systems. This thesis proposes solutions for these problems. Firstly, in analyzing ACSR-VP models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR-VP, but they are difficult to use for large complex system models in practice. In this thesis, we suggest a framework to verify ACSR-VP models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study. Secondly, deadlock checking plays a central role for performing schedulability analysis on real-time systems specified in ACSR-VP. Traditional deadlock checking methods for ACSR-VP raise state space explosion due to flattening data values. This thesis presents a new method to check deadlock for an ACSR-VP specification with a large number of states. We prove that deadlock checking of ACSR-VP can be seen as deadlock checking of transition systems. We propose a new method called VERSA-SAL to link between VERSA and the tool for transition systems called SAL. Lastly, this thesis describes a process algebraic approach to schedulability analysis of hierarchical real-time systems. To facilitate modeling and analyzing hierarchical real-time systems, we conservatively extend an existing process algebraic theory based on ACSR-VP for the schedulability of real-time systems. We explain a method to model a resource model in ACSR which may be partitioned for a subsystem. We also introduce schedulability relation to define the schedulability of hierarchical real-time systems and show that satisfaction checking of the relation is reducible to deadlock checking in ACSR and can be done automatically by the tool support of VERSA. With the schedulability relation, we present algorithms for abstracting real-time system workloads.
more목차
1 Introduction 1
1.1 Model Checking of Real-Time Properties 2
1.2 Symbolic Deadlock Checking 4
1.3 Scheduling Problems of Hierarchical Real-Time Systems 5
2 Schedulability Analysis of Real-Time Systems in ACSR-VP 8
2.1 ACSR-VP 8
2.1.1 Syntax 9
2.1.2 Semantics 12
2.2 Specifying Real-Time Systems in ACSR-VP 16
2.3 Analysis of Real-Time Systems in ACSR-VP 17
3 Model Checking of Real-Time Properties of ACSR-VP 20
3.1 Preliminaries 20
3.1.1 Bisimulation Checking 20
3.1.2 Model Checking 24
State-based vsAction-based Modeling 24
Action-based Model Checking 25
3.2 Model Checking of ACSR-VP Models 27
3.2.1 Translating TLTSs to Abstracted TLTSs 29
3.2.2 Extending ACTL* to Bounded ACTL* 31
3.2.3 Temporal Specification Pattern 33
3.2.4 Tool Chain 33
3.3 Case Study 34
3.3.1 DCM System Description 35
3.3.2 ACSR-VP Models of DCM 35
3.3.3 Model Checking of DCM 38
3.3.4 Discussion 40
4 Symbolic Deadlock Checking of ACSR-VP 43
4.1 Symbolic Semantics of ACSR-VP 43
4.1.1 Symbolic Graph with Assignment 44
4.1.2 Symbolic Operational Semantics 45
4.1.3 Prioritization 49
4.1.4 Deadlocks 50
4.2 Translating Symbolic Graphs to Transition Systems 51
4.2.1 Transition System 52
4.2.2 Translation Function 52
4.2.3 Case Study: Counting Semaphore 55
4.3 Experiment Result 57
4.3.1 Counting Semaphore 59
4.3.2 EDF Scheduling System 61
5 Schedulability Analysis of Hierarchical Real-Time Systems 63
5.1 Modeling Hierarchical Real-Time System in ACSR-VP 63
5.1.1 Task and Workload Model 66
5.1.2 Scheduling Algorithm 68
5.1.3 Resource Model 70
5.2 Schedulability of Hierarchical Real-Time System 71
5.2.1 Schedulability Relation 73
5.2.2 Reduction to Deadlock Checking 77
5.2.3 Case Study 82
5.3 Abstraction of Timing Requirement of Real-Time SystemWorkload 84
5.3.1 Periodic and EDP Abstraction 85
5.3.2 Experimental Results 87
6 Conclusion 92
References 95
