원문정보
초록
영어
In view of the web service model checking application, the combination mode of traditional finite state machines cannot guarantee the correctness of Web composite service. A web service model diction algorithm of non-centralized automaton based on satisfiability modulo theories (SMT) is proposed. First, SMT is used for bounded model checking of time automaton, and the time automaton model is directly converted into logical formula that can be identified by SMT, to make solution; secondly, the proposed SMT time automaton theory is used to achieve the employee travel arrangements web services for modeling and verification; finally, through an example analysis, the effectiveness of the algorithm on the termination of the path deadlock and the optimization of network parameters.
목차
1. Introduction
2. Description of Web Composite Service Problem
2.1. Finite Automaton
2.2. Web Service Barter Transaction System Structure
3. SMT Time Automaton
3.1. SMT Bounded Model Checking
3.2. M Model K Step Path Logic Formula
3.3. The Solution of SMT Logical Formula
4. Experiment and Result Analysis
4.1. Algorithm Model Checking
4.2. Web Service Application Experiment
5. Conclusion
References