SMT有界约束非集中自动机web服务模型检测

SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking

针对web服务模型检测应用中,传统的有限状态机的组合方式无法保证Web组合服务的正确性问题,提出一种基于可满足性模理论(satisfiability modulo theories,SMT)的非集中自动机的web服务模型检测算法。利用SMT对时间自动机进行有界模型检测,将时间自动机模型直接转换成SMT可识别的逻辑公式,并进行求解;利用所提SMT时间自动机理论,实现对雇员出差安排组合web服务进行建模和验证;通过实例分析,验证了算法在解除路径死锁及网络参数指标优化上的有效性。

In model checking for web services applications, the combination of traditional finite state machine cannot guarantee the correctness of web service composition, a method of non centralized automaton model for web service detection algorithm was put forward,based on which could meet of mode theory（satisfiability modulo of the nanocomposite, SMT）. The SMT was used to detect the bounded model of timed automata, and the time automaton was directly converted into SMT identifiable logic formula and was solved; using the SMT timed automata theory, implementation of employee travel arrangements for composite web service was modeled and verified. Through the example analysis, verification of the algorithm in the lifting path deadlocks and network parameters optimization is effective.