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 -