TY - JOUR
T1 - RINGA
T2 - Design and verification of finite state machine for self-adaptive software at runtime
AU - Lee, Euijong
AU - Kim, Young Gab
AU - Seo, Young Duk
AU - Seol, Kwangsoo
AU - Baik, Doo Kwon
N1 - Funding Information:
This research was supported by the Next-Generation Information Computing Development Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Science, ICT & Future Planning ( 2012M3C4A7033346 ). This work also partially was supported by Institute for Information & communications Technology Promotion (IITP) grant funded by the Korea government (MSIP) (No. 2016-0-00498 , User behavior pattern analysis based authentication and anomaly detection within the system using deep learning techniques)
Publisher Copyright:
© 2017 Elsevier B.V.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 2018/1
Y1 - 2018/1
N2 - 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.
AB - 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.
KW - Finite state machine
KW - Model checking
KW - Runtime
KW - Self-adaptive software
UR - http://www.scopus.com/inward/record.url?scp=85029756817&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029756817&partnerID=8YFLogxK
U2 - 10.1016/j.infsof.2017.09.008
DO - 10.1016/j.infsof.2017.09.008
M3 - Article
AN - SCOPUS:85029756817
SN - 0950-5849
VL - 93
SP - 200
EP - 222
JO - Information and Software Technology
JF - Information and Software Technology
ER -