RINGA: Design and verification of finite state machine for self-adaptive software at runtime
- Authors
- Lee, Euijong; Kim, Young-Gab; Seo, Young-Duk; Seol, Kwangsoo; Baik, Doo-Kwon
- Issue Date
- 1월-2018
- Publisher
- ELSEVIER SCIENCE BV
- Keywords
- Self-adaptive software; Model checking; Finite state machine; Runtime
- Citation
- INFORMATION AND SOFTWARE TECHNOLOGY, v.93, pp.200 - 222
- Indexed
- SCIE
SCOPUS
- Journal Title
- INFORMATION AND SOFTWARE TECHNOLOGY
- Volume
- 93
- Start Page
- 200
- End Page
- 222
- URI
- https://scholar.korea.ac.kr/handle/2021.sw.korea/78459
- DOI
- 10.1016/j.infsof.2017.09.008
- ISSN
- 0950-5849
- Abstract
- Context 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. Objective: Model checking is an effective static verification method for software, but existing problems at runtime remain unresolved. In this paper, we propose a self-adaptive software framework that applies model checking to software to enable verification at runtime. Method: 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, we propose two finite state machines 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. Results: We performed an empirical evaluation with several model-checking tools(i.e., NuSMV and CadenceSMV), and the results show that the proposed method is more efficient at runtime. We also investigated a simple example application in six scenarios related to the IoT environment. We implemented Android and Arduino applications, and the results show the practical usability of the proposed self-adaptive framework at runtime. Conclusions: We proposed a framework for integrating model checking with a self-adaptive software lifecycle. The results of our experiments showed that the proposed framework can achieve verify self-adaptation software at runtime.
- Files in This Item
- There are no files associated with this item.
- Appears in
Collections - College of Informatics > Department of Computer Science and Engineering > 1. Journal Articles
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.