TY - GEN
T1 - Runtime verification by convergent formula progression
AU - Shen, Yan
AU - Li, Jianwen
AU - Wang, Zheng
AU - Su, Ting
AU - Fang, Bin
AU - Pu, Geguang
AU - Liu, Wanwei
AU - Chen, Mingsong
N1 - Publisher Copyright:
© 2014 IEEE.
PY - 2014
Y1 - 2014
N2 - Runtime verification is a dynamic verification technique widely used in practice. In this paper we revisit the runtime verification technique with formula progression, which verifies the execution trace step by step by progressing the desired property written in temporal logic. The previous work did not discuss explicitly the bound for the sizes of expanded formulas, while the successive invoking of formula progression is likely to cause divergence. In this paper1, we present the convergent formula progression by introducing a novel fixpoint reduction technique, and prove it guarantees the sizes of expanded formulas be always convergent. To the best of our knowledge, this is the first work discussing the convergence of formula progression. Furthermore, we implement the new runtime verification framework, and experiments show the efficiency of our proposed strategy.
AB - Runtime verification is a dynamic verification technique widely used in practice. In this paper we revisit the runtime verification technique with formula progression, which verifies the execution trace step by step by progressing the desired property written in temporal logic. The previous work did not discuss explicitly the bound for the sizes of expanded formulas, while the successive invoking of formula progression is likely to cause divergence. In this paper1, we present the convergent formula progression by introducing a novel fixpoint reduction technique, and prove it guarantees the sizes of expanded formulas be always convergent. To the best of our knowledge, this is the first work discussing the convergence of formula progression. Furthermore, we implement the new runtime verification framework, and experiments show the efficiency of our proposed strategy.
UR - https://www.scopus.com/pages/publications/84951291675
U2 - 10.1109/APSEC.2014.47
DO - 10.1109/APSEC.2014.47
M3 - 会议稿件
AN - SCOPUS:84951291675
T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC
SP - 255
EP - 262
BT - Proceedings - 21st Asia-Pacific Software Engineering Conference, APSEC 2014
A2 - Gueheneuc, Yann-Gael
A2 - Kwon, Gihwon
A2 - Cha, Sungdeok
PB - IEEE Computer Society
T2 - 21st Asia-Pacific Software Engineering Conference, APSEC 2014
Y2 - 1 December 2014 through 4 December 2014
ER -