Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations

摘要: Abstract Context Model checking is an automatic and precise technique in verification refutation of software hardware systems. Despite its advantages, the state space explosion problem may occur large complex Recent studies demonstrate that using meta-heuristic evolutionary algorithms are a proper solution to handle problem. In systems which specified formally through graph transformations, constructed by applying all enable rules on generated states. such systems, there dependency between each sequence applied space. Objective This fact motivates us use knowledge discovery techniques intelligently explore only portion instead exhaustive exploration. We propose two different acquire form model this paper, we data mining-based approach required obtained from exploring slight Another proposed Bayesian network used capture knowledge. After acquiring knowledge, it employed intelligently, refute property. Results The approaches can be analyze reachability, safety liveness properties. To evaluate approaches, they implemented GROOVE, open source toolset for designing transformations. Conclusion Experimental results set benchmarks show faster more accurate comparison with existing