约束有界模理论非集式Web服务自动机检测

Constrained Bounded Model Theory Based Non-Set-Type Web Services Automaton Detection

在Web服务检测模型实际使用过程中,普通的状态机有界状态组合形式不能确保Web服务组合的准确和有效性,对此提出非集式可满足自动机模理论(SMT),并将其应用到Web模型服务检测过程中。首先,基于SMT算法实现时序有界自动机检测模型,将时序有界自动机转变为可识别SMT公式逻辑,并对其模型参数进行求解;其次,基于时序SMT自动机模型,对单位职工出差进行组合安排,并结合Web服务模型进行检测和算法验证;最后,通过实验对比,表明约束有界模理论非集式Web服务自动机检测算法,能够有效对路径死锁进行解耦,并且可有效实现网络指标参数优化。

In the actual use of Web service detection model, the finite state combination form of general state machine cannot ensure the accuracy and effectiveness of Web service composition, which can be used to meet the automaton mode theory(SMT) and be applied to the Web model. Firstly, based on the SMT algorithm, the timing of the automaton detection model is achieved, and the time series which are bounded to the SMT formula can be transformed into identified formula logic, and its model parameters are solved; Secondly, based on the time series SMT automaton model, the unit staff is arranged on a business trip, and combined with the Web service model, the algorithm is detected and verified; Finally, through the experimental comparison, it is showed that the constrained bounded model theory of non-set Web service automaton detection algorithm can effectively decouple the path deadlock, and can effectively achieve network parameter optimization.