Framework for Self-Adaptive Software: Finite State Machine Modeling and Runtime Verification
Framework for Self-Adaptive Software: Finite State Machine Modeling and Runtime Verification
- 주제(키워드) Self-Adaptive Software , Model-Checking , Finite State Machine , Runtime
- 발행기관 고려대학교 대학원
- 지도교수 백두권
- 발행년도 2018
- 학위수여년월 2018. 8
- 유형 Text
- 학위구분 박사
- 학과 대학원 컴퓨터학과(정보대학)
- 원문페이지 159 p
- 실제URI http://www.dcollection.net/handler/korea/000000081470
- UCI I804:11009-000000081470
- DOI 10.23186/korea.000000081470.11009.0000819
- 본문언어 영어
- 제출원본 000045953680
초록/요약
In recent years, software environments such as the cloud and Internet of Things (IoT) have become increasingly sophisticated, and as a result, development of adaptable software has become very important. Self-adaptive software is appropriate for today’s needs because it changes its behavior or structure in response to a changing environment at runtime. To adapt to changing environments, runtime verification is an important requirement, and research that integrates traditional verification with self-adaptive software is in high demand. Model checking is an effective static verification method for software, but existing problems at runtime remain unresolved. In this dissertation, a self-adaptive software framework is proposed, and it is called RINGA. The proposed framework applies model checking to software to enable verification at runtime. The proposed framework consists of two parts: the design of self-adaptive software using a finite state machine and the adaptation of the software during runtime. For the first part, two finite state machines are proposed for self-adaptive software called the self-adaptive finite state machine (SA-FSM) and abstracted finite state machine (A-FSM). For the runtime verification part, a self-adaptation process based on a MAPE (monitoring, analyzing, planning, and executing) loop is implemented. In addition, a framework based on RINGA is proposed, and a game-theoretic decision-making method is proposed for extracting adaptive strategies under different requirements in an IoT environment. The modeling and the extracting strategies method are used the self-adaptive software framework called RINGA-IoT. An empirical evaluation is performed with several model checking tools (i.e., NuSMV and CadenceSMV), and the results show that the proposed method is more efficient at runtime. In addition, experiments are performed to evaluate the strategy extraction of the RINGA-IoT. The results demonstrate that the RINGA-IoT can be applied at runtime in the IoT environment. Example applications are investigated that are related to the IoT environment. Android and Arduino applications are implemented, and the results show the practical usability of RINGA and RINGA-IoT at runtime. The results of experiments showed that the proposed framework can achieve verify self-adaptation software at runtime.
more목차
ABSTRACT i
1. Introduction 1
1.1 Motivation 1
1.2 Research Purpose 3
1.3 Research Taxonomy 5
1.4 Organization of the Dissertation 10
2. Related Work 11
2.1 Self-Adaptive Software Frameworks 11
2.2 Self-Adaptive Software Platforms 16
2.3 Verification of Self-Adaptive Software 17
2.3 Game Theory 20
3. RINGA: Self-Adaptive Software Framework 22
3.1 Overview of Framework 22
3.2 Model Design 26
3.2.1 Model for Self-Adaptive Software 26
3.2.2 Model for Runtime Verification 29
3.2.3 Algorithm to make A-FSM 33
3.3 MAPE-Loop 43
4. RINGA-IoT: Self adapteive Software Framework for IoT 45
4.1 Overview of RINGA-IoT 46
4.2 Model Design for IoT 48
4.2.1 Classificatoin of IoT Devices 48
4.2.2 Design of Finite State Machine for IoT 49
4.3 Game Theory based Strategy Extraction 57
4.4 Evaluatin Strategies 60
5. Experimental Evalution 62
5.1 Experimental Result of Model Abstraction 62
5.2 Experimental Result of Runtime Verification 68
5.3 Experimental Result of Strategy Extraction 74
6. Proof of Concept 79
6.1 Self-Adaptive Light Control 80
6.1.1Overview of Example Application 80
6.1.2 Modeling of Finite State Machine 82
6.1.3 Arduino Implementation 90
6.1.4 Arduino Implementataion 94
6.1.5 Result of the Example Application 97
6.2 Self-Adaptive IoT Environment 106
6.2.1 Overview of Example Application 106
6.2.2 Arduino Implementation 109
6.2.3 Android Implementation 117
6.2.4 Result of the Example Application 121
7. Conclustion and Future Works 134
7.1 Conclusion 134
7.2 Future Works 136
Bibliography 137
Abstaract (Korean) 146
