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 proceedingConference contribution

3 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 languageEnglish
Title of host publication32nd Annual ACM Symposium on Applied Computing, SAC 2017
PublisherAssociation for Computing Machinery
Pages65-68
Number of pages4
VolumePart F128005
ISBN (Electronic)9781450344869
DOIs
Publication statusPublished - 2017 Apr 3
Event32nd Annual ACM Symposium on Applied Computing, SAC 2017 - Marrakesh, Morocco
Duration: 2017 Apr 42017 Apr 6

Other

Other32nd Annual ACM Symposium on Applied Computing, SAC 2017
CountryMorocco
CityMarrakesh
Period17/4/417/4/6

Fingerprint

Model checking
Processing
Experiments

Keywords

  • Model checking
  • Self-adaptive software
  • Transition system

ASJC Scopus subject areas

  • Software

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 (Vol. Part F128005, pp. 65-68). 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; Seol, Kwangsoo; Baik, Doo Kwon.

32nd Annual ACM Symposium on Applied Computing, SAC 2017. Vol. Part F128005 Association for Computing Machinery, 2017. p. 65-68.

Research output: Chapter in Book/Report/Conference proceedingConference 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. 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
Lee E, Kim YG, Seo YD, Seol K, Baik DK. Runtime verification method for self-adaptive software using reachability of transition system model. In 32nd Annual ACM Symposium on Applied Computing, SAC 2017. Vol. Part F128005. Association for Computing Machinery. 2017. p. 65-68 https://doi.org/10.1145/3019612.3019851
Lee, Euijong ; Kim, Young Gab ; Seo, Young Duk ; Seol, Kwangsoo ; Baik, Doo Kwon. / Runtime verification method for self-adaptive software using reachability of transition system model. 32nd Annual ACM Symposium on Applied Computing, SAC 2017. Vol. Part F128005 Association for Computing Machinery, 2017. pp. 65-68
@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}",
year = "2017",
month = "4",
day = "3",
doi = "10.1145/3019612.3019851",
language = "English",
volume = "Part F128005",
pages = "65--68",
booktitle = "32nd Annual ACM Symposium on Applied Computing, SAC 2017",
publisher = "Association for Computing Machinery",

}

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

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

VL - Part F128005

SP - 65

EP - 68

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

PB - Association for Computing Machinery

ER -