RINGA: Design and verification of finite state machine for self-adaptive software at runtime
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Lee, Euijong | - |
dc.contributor.author | Kim, Young-Gab | - |
dc.contributor.author | Seo, Young-Duk | - |
dc.contributor.author | Seol, Kwangsoo | - |
dc.contributor.author | Baik, Doo-Kwon | - |
dc.date.accessioned | 2021-09-02T17:04:15Z | - |
dc.date.available | 2021-09-02T17:04:15Z | - |
dc.date.created | 2021-06-16 | - |
dc.date.issued | 2018-01 | - |
dc.identifier.issn | 0950-5849 | - |
dc.identifier.uri | https://scholar.korea.ac.kr/handle/2021.sw.korea/78459 | - |
dc.description.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. | - |
dc.language | English | - |
dc.language.iso | en | - |
dc.publisher | ELSEVIER SCIENCE BV | - |
dc.subject | QUANTITATIVE VERIFICATION | - |
dc.subject | ADAPTATION | - |
dc.title | RINGA: Design and verification of finite state machine for self-adaptive software at runtime | - |
dc.type | Article | - |
dc.contributor.affiliatedAuthor | Baik, Doo-Kwon | - |
dc.identifier.doi | 10.1016/j.infsof.2017.09.008 | - |
dc.identifier.scopusid | 2-s2.0-85029756817 | - |
dc.identifier.wosid | 000414878200013 | - |
dc.identifier.bibliographicCitation | INFORMATION AND SOFTWARE TECHNOLOGY, v.93, pp.200 - 222 | - |
dc.relation.isPartOf | INFORMATION AND SOFTWARE TECHNOLOGY | - |
dc.citation.title | INFORMATION AND SOFTWARE TECHNOLOGY | - |
dc.citation.volume | 93 | - |
dc.citation.startPage | 200 | - |
dc.citation.endPage | 222 | - |
dc.type.rims | ART | - |
dc.type.docType | Article | - |
dc.description.journalClass | 1 | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Information Systems | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.subject.keywordPlus | QUANTITATIVE VERIFICATION | - |
dc.subject.keywordPlus | ADAPTATION | - |
dc.subject.keywordAuthor | Self-adaptive software | - |
dc.subject.keywordAuthor | Model checking | - |
dc.subject.keywordAuthor | Finite state machine | - |
dc.subject.keywordAuthor | Runtime | - |
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
(02841) 서울특별시 성북구 안암로 14502-3290-1114
COPYRIGHT © 2021 Korea University. All Rights Reserved.
Certain data included herein are derived from the © Web of Science of Clarivate Analytics. All rights reserved.
You may not copy or re-distribute this material in whole or in part without the prior written consent of Clarivate Analytics.