Runtime verification method for self-adaptive software using reachability of transition system model

Euijong Lee; Young Gab Kim; Young Duk Seo; Kwangsoo Seol; Doo Kwon Baik

doi:10.1145/3019612.3019851

Runtime verification method for self-adaptive software using reachability of transition system model

Euijong Lee, Young Gab Kim, Young Duk Seo, Kwangsoo Seol, Doo Kwon Baik

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

Abstract

Self-adaptive software can change its own behavior in order to achieve an intended objective in a changing environment. Consequently, self-adaptive software requires practical runtime verification and validation. We propose an approach for runtime verification of self-adaptive software by using a designed transition system model. The proposed approach consists of two phases: pre-computing phase and runtime phase. In the precomputing phase, we assume that the self-adaptive software is designed as a transition system. In this phase, the proposed approach translates the designed transition system into equations for runtime verification. For translation, we suggest an algorithm based on state elimination and reachability. After the pre-computing phase, the results of the translated equations are verified in the runtime phase. In order to demonstrate the suitability of our proposed approach, we performed experiments to evaluate the performance of the pre-processing phase and the runtime phase. In comparison with other model-checking tools, our approach achieved excellent results.

Original language	English
Title of host publication	32nd Annual ACM Symposium on Applied Computing, SAC 2017
Publisher	Association for Computing Machinery
Pages	65-68
Number of pages	4
ISBN (Electronic)	9781450344869
DOIs	https://doi.org/10.1145/3019612.3019851
Publication status	Published - 2017 Apr 3
Event	32nd Annual ACM Symposium on Applied Computing, SAC 2017 - Marrakesh, Morocco Duration: 2017 Apr 4 → 2017 Apr 6

Publication series

Name	Proceedings of the ACM Symposium on Applied Computing
Volume	Part F128005

Other

Other	32nd Annual ACM Symposium on Applied Computing, SAC 2017
Country/Territory	Morocco
City	Marrakesh
Period	17/4/4 → 17/4/6

Bibliographical note

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 (NRF 2012M3C4A7033346).

Publisher Copyright:
Copyright 2017 ACM.

Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.

Keywords

Model checking
Self-adaptive software
Transition system

ASJC Scopus subject areas

Software

Access to Document

10.1145/3019612.3019851

Cite this

Lee, E., Kim, Y. G., Seo, Y. D., Seol, K., & Baik, D. K. (2017). Runtime verification method for self-adaptive software using reachability of transition system model. In 32nd Annual ACM Symposium on Applied Computing, SAC 2017 (pp. 65-68). (Proceedings of the ACM Symposium on Applied Computing; Vol. Part F128005). Association for Computing Machinery. https://doi.org/10.1145/3019612.3019851

Runtime verification method for self-adaptive software using reachability of transition system model. / Lee, Euijong; Kim, Young Gab; Seo, Young Duk et al.
32nd Annual ACM Symposium on Applied Computing, SAC 2017. Association for Computing Machinery, 2017. p. 65-68 (Proceedings of the ACM Symposium on Applied Computing; Vol. Part F128005).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Lee, E, Kim, YG, Seo, YD, Seol, K & Baik, DK 2017, Runtime verification method for self-adaptive software using reachability of transition system model. in 32nd Annual ACM Symposium on Applied Computing, SAC 2017. Proceedings of the ACM Symposium on Applied Computing, vol. Part F128005, Association for Computing Machinery, pp. 65-68, 32nd Annual ACM Symposium on Applied Computing, SAC 2017, Marrakesh, Morocco, 17/4/4. https://doi.org/10.1145/3019612.3019851

@inproceedings{7d726394c4f442ba8a316062562f697d,

title = "Runtime verification method for self-adaptive software using reachability of transition system model",

abstract = "Self-adaptive software can change its own behavior in order to achieve an intended objective in a changing environment. Consequently, self-adaptive software requires practical runtime verification and validation. We propose an approach for runtime verification of self-adaptive software by using a designed transition system model. The proposed approach consists of two phases: pre-computing phase and runtime phase. In the precomputing phase, we assume that the self-adaptive software is designed as a transition system. In this phase, the proposed approach translates the designed transition system into equations for runtime verification. For translation, we suggest an algorithm based on state elimination and reachability. After the pre-computing phase, the results of the translated equations are verified in the runtime phase. In order to demonstrate the suitability of our proposed approach, we performed experiments to evaluate the performance of the pre-processing phase and the runtime phase. In comparison with other model-checking tools, our approach achieved excellent results.",

keywords = "Model checking, Self-adaptive software, Transition system",

author = "Euijong Lee and Kim, {Young Gab} and Seo, {Young Duk} and Kwangsoo Seol and Baik, {Doo Kwon}",

note = "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 (NRF 2012M3C4A7033346). Publisher Copyright: Copyright 2017 ACM. Copyright: Copyright 2018 Elsevier B.V., All rights reserved.; 32nd Annual ACM Symposium on Applied Computing, SAC 2017 ; Conference date: 04-04-2017 Through 06-04-2017",

year = "2017",

month = apr,

day = "3",

doi = "10.1145/3019612.3019851",

language = "English",

series = "Proceedings of the ACM Symposium on Applied Computing",

publisher = "Association for Computing Machinery",

pages = "65--68",

booktitle = "32nd Annual ACM Symposium on Applied Computing, SAC 2017",

}

TY - GEN

T1 - Runtime verification method for self-adaptive software using reachability of transition system model

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 (NRF 2012M3C4A7033346). Publisher Copyright: Copyright 2017 ACM. Copyright: Copyright 2018 Elsevier B.V., All rights reserved.

PY - 2017/4/3

Y1 - 2017/4/3

N2 - Self-adaptive software can change its own behavior in order to achieve an intended objective in a changing environment. Consequently, self-adaptive software requires practical runtime verification and validation. We propose an approach for runtime verification of self-adaptive software by using a designed transition system model. The proposed approach consists of two phases: pre-computing phase and runtime phase. In the precomputing phase, we assume that the self-adaptive software is designed as a transition system. In this phase, the proposed approach translates the designed transition system into equations for runtime verification. For translation, we suggest an algorithm based on state elimination and reachability. After the pre-computing phase, the results of the translated equations are verified in the runtime phase. In order to demonstrate the suitability of our proposed approach, we performed experiments to evaluate the performance of the pre-processing phase and the runtime phase. In comparison with other model-checking tools, our approach achieved excellent results.

AB - Self-adaptive software can change its own behavior in order to achieve an intended objective in a changing environment. Consequently, self-adaptive software requires practical runtime verification and validation. We propose an approach for runtime verification of self-adaptive software by using a designed transition system model. The proposed approach consists of two phases: pre-computing phase and runtime phase. In the precomputing phase, we assume that the self-adaptive software is designed as a transition system. In this phase, the proposed approach translates the designed transition system into equations for runtime verification. For translation, we suggest an algorithm based on state elimination and reachability. After the pre-computing phase, the results of the translated equations are verified in the runtime phase. In order to demonstrate the suitability of our proposed approach, we performed experiments to evaluate the performance of the pre-processing phase and the runtime phase. In comparison with other model-checking tools, our approach achieved excellent results.

KW - Model checking

KW - Self-adaptive software

KW - Transition system

UR - http://www.scopus.com/inward/record.url?scp=85020882096&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85020882096&partnerID=8YFLogxK

U2 - 10.1145/3019612.3019851

DO - 10.1145/3019612.3019851

M3 - Conference contribution

AN - SCOPUS:85020882096

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 65

EP - 68

BT - 32nd Annual ACM Symposium on Applied Computing, SAC 2017

PB - Association for Computing Machinery

T2 - 32nd Annual ACM Symposium on Applied Computing, SAC 2017

Y2 - 4 April 2017 through 6 April 2017

ER -

Runtime verification method for self-adaptive software using reachability of transition system model

Abstract

Publication series

Other

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this