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

系统仿真学报 ›› 2016, Vol. 28 ›› Issue (9): 2283-2288.

• 短文 • 上一篇

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

韦容¹, 申希兵¹, 杨毅²

1.钦州学院人文学院,广西钦州 535000;
2.广西科技大学软件学院,广西柳州 545006

收稿日期:2015-06-10 修回日期:2015-07-24 出版日期:2016-09-08 发布日期:2020-08-14
作者简介:韦容(1982-),女,广西上林,硕士生,高工,研究方向为网络安全及系统分析、计算机图形学;申希兵(1981-),男,山东沂水,硕士,讲师,研究方向为地理信息系统;杨毅(1975-),男,广西贵港,硕士,讲师,研究方向为人工智能。

SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking

Wei Rong¹, Shen Xibing¹, Yang Yi²

1. College of Humanities , Qinzhou University, Qinzhou 535000, China;
2. College of Software, Guangxi University of Science and Technology, Liuzhou 545006, China

Received:2015-06-10 Revised:2015-07-24 Online:2016-09-08 Published:2020-08-14

摘要/Abstract

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

关键词: 可满足性模理论, 自动机, web服务, 模型检测, 大数据

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

中图分类号:

TP391

韦容, 申希兵, 杨毅. SMT有界约束非集中自动机web服务模型检测[J]. 系统仿真学报, 2016, 28(9): 2283-2288.

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.

参考文献 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]	孙一铃, 陈谊, 单桂华, 李晓兴. 基于AR技术的多人互动地球仪系统[J]. 系统仿真学报, 2022, 34(6): 1367-1374.
[2]	蒋阳升, 王思琛, 高宽, 刘梦, 姚志洪. 混入智能网联车队的混合交通流元胞自动机模型[J]. 系统仿真学报, 2022, 34(5): 1025-1032.
[3]	张振海, 姚婕. 基于时间自动机的C3+ATO系统场景建模与验证[J]. 系统仿真学报, 2021, 33(4): 951-961.
[4]	刘展宏, 杨秀建, 吴相稷, 黄震. 基于元胞自动机的雾天车辆跟驰建模与仿真[J]. 系统仿真学报, 2021, 33(10): 2399-2410.
[5]	刘宗杨, 周春辉, 赵俊男, 肖进丽, 甘浪雄. 基于元胞自动机的航道通过能力建模与仿真[J]. 系统仿真学报, 2021, 33(10): 2478-2487.
[6]	宋英华, 张宇, 霍非舟, 吕伟, 马亚萍. 考虑避让行为的人员疏散元胞自动机模型研究[J]. 系统仿真学报, 2020, 32(6): 975-981.
[7]	周国雄, 李彤, 陈爱斌, 何明芳. 森林灭火水源选址的建模与仿真[J]. 系统仿真学报, 2020, 32(4): 660-668.
[8]	邢志伟, 徐铭怡, 罗晓, 罗谦. 飞机滑行路径仿真与优化研究[J]. 系统仿真学报, 2020, 32(2): 323-331.
[9]	孙正霖, 袁伟强, 李蔚清. 基于可接受性标准的复杂产品仿真系统在线评估框架[J]. 系统仿真学报, 2020, 32(12): 2324-2331.
[10]	胡杨, 张小咏, 肖迪. 基于手机大数据的城市建筑物人口时空估算[J]. 系统仿真学报, 2020, 32(10): 1874-1883.
[11]	黄子赫, 高尚兵, 潘志庚, 惠浩, 廖麒羽, 赵锋锋. 基于快速密度聚类的载客热点可视化分析方法[J]. 系统仿真学报, 2019, 31(7): 1429-1438.
[12]	司光亚, 王飞, 刘洋. 基于仿真大数据的体系分析方法研究[J]. 系统仿真学报, 2019, 31(3): 511-519.
[13]	孔源, 杜怡曼, 吴建平, 胡可臻. 基于浮动车大数据的电动汽车潜在用户分析[J]. 系统仿真学报, 2019, 31(3): 575-584.
[14]	肖迪, 张小咏, 胡杨. 基于手机大数据的城市功能区识别方法[J]. 系统仿真学报, 2019, 31(11): 2281-2288.
[15]	张会丽, 李志河. 一种基于HNN的云服务组合优化[J]. 系统仿真学报, 2019, 31(11): 2335-2343.

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

SMT Bounded Constrained Non Centralized Automaton Web Service Model Checking

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献 12

相关文章 15

编辑推荐

Metrics

本文评价