A Hybrid Model Checking and Runtime Monitoring Method for C++ Web Services

Traditional model checking methods to find safety and liveness violations are usually applied in the abstract model, while existing runtime monitoring methods to check the predicates can not obtain the high path coverage. This paper presents a hybrid model checking and runtime monitoring method to check the safety and liveness properties in real complex distributed C/C++ Web service systems,which can offer both a richer and more efficient way to search violations specified by linear temporal logic. Based on our model checking engine to walk different paths, we adopt the finite linear temporal logic engine to dynamically verify properties in C/C++ Web service systems. Then, we use the practical examples to illustrate its usage and applications in real C/C++ Web service systems.