论文部分内容阅读
针对web服务模型检测应用中,传统的有限状态机的组合方式无法保证Web组合服务的正确性问题,提出一种基于可满足性模理论(satisfiability modulo theories,SMT)的非集中自动机的web服务模型检测算法。利用SMT对时间自动机进行有界模型检测,将时间自动机模型直接转换成SMT可识别的逻辑公式,并进行求解;利用所提SMT时间自动机理论,实现对雇员出差安排组合web服务进行建模和验证;通过实例分析,验证了算法在解除路径死锁及网络参数指标优化上的有效性。
In the application of web service model detection, the combination of traditional finite state machines can not guarantee the correctness of web composition services. A non-centralized automaton web service based on satisfiability modulo theories (SMT) Model detection algorithm. Use SMT to detect the bounded model of the time automaton, transform the time automaton model directly into the identifiable logic formula of SMT, and solve it; use the proposed SMT time automaton theory to realize the employee’s business trip to arrange the combination of web services Through the example analysis, the validity of the algorithm in solving the deadlock of the path and the optimization of network parameters is verified.