SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking

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.

Key words: satisfiability modulo theories, automata, Web service, model checking, big data

CLC Number:

TP391

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.

References 12

[1]	Sharma, Meenakshi, Siddiqui, Adil.RFID based mobiles: Next generation applications[C]// IEEE Xplore The 2nd IEEE International Conference on Information Management and Engineering, Chengdu, China, April 2010. USA: IEEE Xplore, 2010: 523-526.
[2]	Walter B, Ion C Boi.Decentralized Orchestration of Composite Web Services[C]// Proceedings of IEEE International Conference on Web Services (ICWS'06). Chicago, IL, USA. USA: IEEE, 2006.
[3]	Ekwall R, Mena S, Pleisch S.Towards Flexible Finate State Machine Based Protocol Composition[C]// Proceedings of Third IEEE International Symposium on Network Computing and Applications (NCA’04), Boston, USA. USA: IEEE, 2004.
[4]	Girish C, Sunil C, Vijay M.Decentralized Orchestration of Composite Web Services [C]// International World Wide Web Conference on Alternate Track Papers and Posters, New York, NY, USA: ACM Press, 2004: 134-143.
[5]	于守健, 何丰, 乐嘉锦. 基于接口匹配的Web 服务自动组合[J]. 计算机科学, 2007, 34(3): 61-68.
[6]	Gerede C E, Hull R, Ibarra O H.Automated Composition of Eservices: Lookaheads[C]// Proceedings of 2nd International Conference on Service-Oriented Computing. NewYork, NY, USA: ACM, 2004: 252-262.
[7]	于守健, 李卫民, 吴国文. BPEL中基于有限状态自动机的Web 服务自动组合[J]. 小型微型计算机系统, 2007, 28(4): 742-747.
[8]	Diego Zuquim, Guimar Garcia, Maria Beatriz.Quality of Service Management for Web Service Compositions[C]// Proceedings of 11th IEEE International Conference on Computational Science and Engineering, Sao Paulo, Brazil, 2008. USA: IEEE, 2008:189-196.
[9]	张耀峰, 肖人彬. 基于元胞自动机的网络群体事件舆论同步的涌现机制[J]. 系统工程理论与实践, 2014, 34(10): 2600-2608.
[10]	Kaiyu Wang, Naishuo Tian.Performance Modeling of Composite Web Services[C]// Proceedings of 2009 Pacific-Asia Conference on Circuits, Communications and System, 2009, Chengdu, China: PACCS 2009:127-130.
[11]	朱昶胜, 王兵, 黄军强. 元胞自动机交通流NS模型相图研究[J]. 计算机工程与应用, 2014, 50(21): 48-53.
[12]	Liangzhao Zeng, Boualem B, Marlon D.Quality Driven Web Services Composition[C]// Proceedings of 12th Int'l Conference on World Wide Web( WWW'03), New York, NY, USA: ACM, 2003: 411-421.

[1]	Yiling Sun, Yi Chen, Guihua Shan, Xiaoxing Li. Multi-person Interactive Globe System Based on AR Technology [J]. Journal of System Simulation, 2022, 34(6): 1367-1374.
[2]	Yangsheng Jiang, Sichen Wang, Kuan Gao, Meng Liu, Zhihong Yao. Cellular Automata Model of Mixed Traffic Flow Composed of Intelligent Connected Vehicles’ Platoon [J]. Journal of System Simulation, 2022, 34(5): 1025-1032.
[3]	Zhang Zhenhai, Yao Jie. Modeling and Verification of Scene of C3+ATO System Based on Timed Automata [J]. Journal of System Simulation, 2021, 33(4): 951-961.
[4]	Liu Zhanhong, Yang Xiujian, Wu Xiangji, Huang Zhen. Modeling and Simulation of Car Following in Fog Based on Cellular Automata [J]. Journal of System Simulation, 2021, 33(10): 2399-2410.
[5]	Liu Zongyang, Zhou Chunhui, Zhao Junnan, Xiao Jinli, Gan Langxiong. Modeling and Simulation of Channel Passage Capacity Based on Cellular Automata [J]. Journal of System Simulation, 2021, 33(10): 2478-2487.
[6]	Song Yinghua, Zhang Yu, Huo Feizhou, Lü Wei, Ma Yaping. Study on Evacuation Cellular Automaton Model Considering Avoidance Behavior [J]. Journal of System Simulation, 2020, 32(6): 975-981.
[7]	Xing Zhiwei, Xu Mingyi, Luo Xiao, Luo Qian. Simulation and Optimization of Aircraft Sliding Path [J]. Journal of System Simulation, 2020, 32(2): 323-331.
[8]	Hu Yang, Zhang Xiaoyong, Xiao Di. Estimation of Space-time of Urban Building Population Based on Mobile Phone Big Data [J]. Journal of System Simulation, 2020, 32(10): 1874-1883.
[9]	Huang Zihe, Gao Shangbing, Pan Zhigeng, Hui Hao, Liao Qiyu, Zhao Fengfeng. Visualization Analysis Method of Passenger Hotspot Based on Fast Density Clustering [J]. Journal of System Simulation, 2019, 31(7): 1429-1438.
[10]	Si Guangya, Wang Fei, Liu Yang. System Analysis Method Based on Simulation Big Data [J]. Journal of System Simulation, 2019, 31(3): 511-519.
[11]	Kong Yuan, Du Yiman, Wu Jianping, Hu Kezhen. Potential Users of Battery Electric Vehicle Based on Big Data of Floating Vehicles [J]. Journal of System Simulation, 2019, 31(3): 575-584.
[12]	Xiao Di, Zhang Xiaoyong, Hu Yang. Urban Functional Area Identification Method Based on Mobile Big Data [J]. Journal of System Simulation, 2019, 31(11): 2281-2288.
[13]	Zhang Huili, Li Zhihe. A Cloud Service Composition Optimization Based on HNN [J]. Journal of System Simulation, 2019, 31(11): 2335-2343.
[14]	Li Li, Zhu Yongli, Song Yaqi. Parallel Pattern Recognition of Leak Current Data Using Spark-KNN [J]. Journal of System Simulation, 2018, 30(4): 1473-1481.
[15]	Zhou Guoxiong, Wu Qi, Chen Aibin. Forestry Fire Spatial Diffusion Model Based on Multi-Agent Algorithm with Cellular Automata [J]. Journal of System Simulation, 2018, 30(3): 824-831.