TY - GEN
T1 - A novel approach of CTL model checking based on probe machine
AU - Wang, Dong
AU - Liu, Jing
AU - Xu, Jin
AU - Sun, Haiying
AU - Kang, Jiexiang
N1 - Publisher Copyright:
© 2021 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2021
Y1 - 2021
N2 - Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. However, the state space may be extremely large for many practical systems, and this is a major limitation for state-space search algorithms in model checking. We have proposed a novel computing model called probe machine in 2016, which is a fully parallel computing model. In comparison to the Turing machine, it can solve the graph search problems efficiently, which can overcome the existing model checking limitations. In this paper, we propose a novel approach to perform Computation Tree Logic (CTL) model checking based on the mathematical model of probe machine, which can verify all CTL properties. It can greatly reduce the verification time for systems with large state space. We develop a model checker called CTL2PROBE based on our approach and the experimental results show that our approach is better than NuSMV.
AB - Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. However, the state space may be extremely large for many practical systems, and this is a major limitation for state-space search algorithms in model checking. We have proposed a novel computing model called probe machine in 2016, which is a fully parallel computing model. In comparison to the Turing machine, it can solve the graph search problems efficiently, which can overcome the existing model checking limitations. In this paper, we propose a novel approach to perform Computation Tree Logic (CTL) model checking based on the mathematical model of probe machine, which can verify all CTL properties. It can greatly reduce the verification time for systems with large state space. We develop a model checker called CTL2PROBE based on our approach and the experimental results show that our approach is better than NuSMV.
KW - Computation tree logic
KW - Graph search
KW - Model checking
KW - Probe machine
UR - https://www.scopus.com/pages/publications/85114278111
U2 - 10.18293/SEKE2021-139
DO - 10.18293/SEKE2021-139
M3 - 会议稿件
AN - SCOPUS:85114278111
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 183
EP - 188
BT - Proceedings - SEKE 2021
PB - Knowledge Systems Institute Graduate School
T2 - 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021
Y2 - 1 July 2021 through 10 July 2021
ER -