SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking

Authors

Wei Rong, 1. College of Humanities , Qinzhou University, Qinzhou 535000, China;;
Xibing Shen, 1. College of Humanities , Qinzhou University, Qinzhou 535000, China;;
Yang Yi, 2. College of Software, Guangxi University of Science and Technology, Liuzhou 545006, China;

Abstract

Abstract: 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.

Recommended Citation

Rong, Wei; Shen, Xibing; and Yi, Yang (2020) "SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking," Journal of System Simulation: Vol. 28: Iss. 9, Article 51.
Available at: https://dc-china-simulation.researchcommons.org/journal/vol28/iss9/51

First Page

2283

Revised Date

2015-07-24

DOI Link

https://doi.org/

Last Page

2288

CLC

TP391

Recommended Citation

Wei Rong, Shen Xibing, Yang Yi. SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking[J]. Journal of System Simulation, 2016, 28(9): 2283-2288.