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

发布时间：2018-08-24 09:26

【摘要】：针对web服务模型检测应用中,传统的有限状态机的组合方式无法保证Web组合服务的正确性问题,提出一种基于可满足性模理论(satisfiability modulo theories,SMT)的非集中自动机的web服务模型检测算法。利用SMT对时间自动机进行有界模型检测,将时间自动机模型直接转换成SMT可识别的逻辑公式,并进行求解;利用所提SMT时间自动机理论,实现对雇员出差安排组合web服务进行建模和验证;通过实例分析,验证了算法在解除路径死锁及网络参数指标优化上的有效性。
[Abstract]:In order to solve the problem that the traditional finite state machine (FSM) composition method can not guarantee the correctness of Web composition services in web service model detection applications, a web service model detection algorithm based on satisfiability module theory (satisfiability modulo theories,SMT) is proposed. The bounded model of time automata is checked by SMT, and the time automaton model is transformed directly into the logical formula recognizable by SMT and solved, and the theory of SMT time automaton is used to solve the problem. The modeling and verification of employee travel arrangement composition web service is realized, and the effectiveness of the algorithm in the optimization of path deadlock and network parameter index is verified by an example analysis.
【作者单位】： 钦州学院人文学院;广西科技大学软件学院;
【分类号】：TP393.09

【相似文献】

相关期刊论文 前10条

1 周立青;杨晋吉;;乐观合同签订协议的模型检测分析[J];计算机工程;2011年07期

2 徐畅;刘吉锋;孙吉贵;;基于经典逻辑的安全协议模型检测方法[J];计算机科学;2008年06期

3 钮俊;曾国荪;王伟;;基于模型检测的时间空间性能验证方法[J];计算机学报;2010年09期

4 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期

5 唐郑熠;许道云;王晓峰;王正才;;基于模型检测技术的语义Web服务自动组合[J];吉林大学学报(工学版);2013年02期

6 陈小峰;冯登国;;可信密码模块的模型检测分析[J];通信学报;2010年01期

7 吕审;;基于模型检测的密码协议安全性的实际应用[J];电脑知识与技术;2011年09期

8 张冬梅,马华东,高大永;基于Uppaal的移动IPv6协议的模型检测[J];北京邮电大学学报;2005年04期

9 马怀磊;郭华;庄雷;;基于模型检测的不可靠环境下电子商务协议分析[J];计算机工程与科学;2007年10期

10 刘如娟;戴桂兰;胡长军;白晓颖;;Web服务的模型检测技术探讨[J];小型微型计算机系统;2007年11期

相关博士学位论文 前1条

1 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

相关硕士学位论文 前10条

1 于文光;一种基于BDD的语义Web服务组装规划器的设计与实现[D];北京大学;2008年

2 郭华;基于模型检测的电子商务协议形式化验证方法研究[D];郑州大学;2006年

3 王敏飞;模型检测在安全协议验证中的研究与应用[D];南京航空航天大学;2009年

4 刘吉锋;一个新的基于SAT方法的安全协议模型检测算法[D];吉林大学;2007年

5 陈艳;基于时态认知逻辑的Web服务模型检测[D];桂林电子科技大学;2009年

6 郭肇毅;基于模型检测的形式化协议验证[D];电子科技大学;2012年

7 万子龙;基于模型检测的SET协议形式化验证与改进[D];南昌大学;2014年

8 谭志华;网络认证协议的高效模型检测研究[D];湖南大学;2011年

9 黄瑛;SET协议支付过程分析及模型检测[D];贵州大学;2006年

10 阮小黎;基于模型检测的C语言安全信息流研究[D];清华大学;2007年

，

本文编号：2200381