基于进程迹的CSP模型验证框架

发布时间：2018-06-14 11:01

  本文选题：通信顺序进程(CSP) + 并发系统　； 参考：《计算机科学》2013年11期

【摘要】：CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。
[Abstract]:CSP Communication process is a classic method for building concurrent systems and network security protocols. The current mainstream CSP model verification methods need to transform the process into a migration system, the transformation process is more complex, and the properties of CSP model are standardized, which is not conducive to the description of activity. A CSP model verification framework based on process trace is proposed. Its properties are described by the universal specification method LTL. A CSP verification system is implemented by using the ASPU Answer set programming technology. The experimental results show that the proposed system has better description ability and higher accuracy than similar systems, and can provide counterexample when its properties are not satisfied.
【作者单位】： 桂林电子科技大学计算机科学与工程学院;
【基金】：国家自然科学基金(61262008,61063002) 广西自然基金(2011GXNSFA018166,2011GXNSFA018164) 广西可信软件重点实验室基金(kx201113)资助
【分类号】：TP393.08

【参考文献】

相关期刊论文 前1条

1 赵岭忠;张超;钱俊彦;;基于ASP的CSP并发系统验证研究[J];计算机科学;2012年12期

【共引文献】

相关期刊论文 前10条

1 李仲侠;通信业务自然描述方法的研究[J];长春邮电学院学报;1997年03期

2 赵波，李文;C程序递归变换预编译系统的设计[J];大连铁道学院学报;1996年01期

3 李文，朱力鸣;分层递阶智能控制任务转换模型的研究现状[J];大连铁道学院学报;1996年02期

4 刘树锟;莫正杰;吴沛林;黄小波;;基于Java建模语言的不变量检测工具[J];电脑开发与应用;2012年05期

5 张宇;平龙妹;;基于敏捷建模的形式化需求分析方法[J];电脑知识与技术;2008年34期

6 林添荣;蒋建民;;UML活动图的一种逻辑语义[J];福建师范大学学报(自然科学版);2010年03期

7 刘富春;方程逻辑Institution理论及其性质[J];广东有色金属学报;2005年01期

8 李侃，王兵山，，李舟军;并发面向对象语言的演算语义研究[J];国防科技大学学报;1996年01期

9 王彩芬;程序正确性证明及循环不变式的寻找方法[J];甘肃科学学报;2000年03期

10 白金山;杜习慧;赵莉莉;李祥;;并发程序验证器CPV的设计与应用研究[J];贵州大学学报(自然科学版);2008年01期

相关会议论文 前2条

1 柳永坡;晏海华;张懋;刘雪梅;;测试流程管理与监控技术的研究与实现[A];第五届中国测试学术会议论文集[C];2008年

2 姚丹霖;殷建平;;大型汉英双语电子词典的结构与自动生成[A];数据库研究进展97——第十四届全国数据库学术会议论文集（下）[C];1997年

相关博士学位论文 前10条

1 吴新星;基于语言的软件可信性度量理论及其应用[D];华东师范大学;2011年

2 代飞;基于EPMM的软件演化过程模型验证[D];云南大学;2011年

3 陈晓江;分布式系统软件体系结构建模与开发方法研究[D];西北大学;2010年

4 曾颖;基于抽象解释的软件保护相关问题研究[D];解放军信息工程大学;2011年

5 郭健强;面向对象软件测试理论与技术的研究[D];西安电子科技大学;1999年

6 李广元;LTLC：面向实时与混成系统的连续时序逻辑[D];中国科学院软件研究所;2001年

7 艾萍;构件柔性组装描述的形式化方法研究及其在水利领域的应用[D];河海大学;2002年

8 郑红;分布式系统形式化建模技术研究[D];中国科学院研究生院（软件研究所）;2003年

9 胡瑜;基于有色Petri网理论的并行自动测试系统建模研究[D];电子科技大学;2003年

10 徐晓泉;完备格的关系表示理论及其应用[D];四川大学;2004年

相关硕士学位论文 前10条

1 朱恒亮;SOA中服务与服务组合的形式化研究[D];福建师范大学;2010年

2 杨志财;安全策略的形式化描述及其可视化实现[D];东北师范大学;2011年

3 李超;基于扩展下推自动机的Java程序安全相关行为模型自动生成[D];东北师范大学;2011年

4 费利明;基于JVMTI实现安全策略的强制实施[D];东北师范大学;2011年

5 郑建丹;基于组件的逐步求精程序设计方法[D];中国科学院软件研究所;2001年

6 孙晓舟;HLR设计方法研究[D];西安电子科技大学;2002年

7 宁爱兵;面向事实程序设计的构思[D];江西师范大学;2003年

8 吴海涛;对象并发演算模型及对象语言语义研究[D];郑州大学;2003年

9 王振;MSC前台进程对象化方法研究[D];南京理工大学;2004年

10 崔海渤;Java语言的类和多态性的公理语义[D];大连理工大学;2005年

【二级参考文献】

相关期刊论文 前1条

1 张兆庆,蒋昌俊,乔如良,叶志宝,周杰;PVM并行程序验证系统的原理与实现[J];计算机学报;1999年04期

【相似文献】

相关期刊论文 前10条

1 李杨;程建华;房鼎益;陈晓江;冯健;;并发系统的安全性与活性的验证方法[J];计算机工程与应用;2008年04期

2 吴丘林;;一种自顶而下的Web-服务全局行为设计方法[J];电脑知识与技术(学术交流);2007年10期

3 李海鹰,程灏,叶为全,庄镇泉;基于协同侦测技术的移动主体模型验证策略研究[J];计算机学报;2005年05期

4 袁勇福;高春鸣;刘荣胜;;Web服务组合的互模拟验证[J];计算机应用;2006年10期

5 蒋昌俊，郑应平，疏松桂;并发系统建模与分析研究[J];高技术通讯;1996年06期

6 许可;王跃宣;吴澄;;网格服务链模型的验证分析技术及应用[J];中国科学(E辑:信息科学);2007年04期

7 辜希武;卢正鼎;;基于Pi-演算的BPEL4 WS Web服务组合形式化模型[J];计算机科学;2007年03期

8 周昆;金可音;;一种Web服务组合形式化模型及验证方法[J];微计算机信息;2010年30期

9 刘一静;谢鸿波;吴远成;;安全协议认证属性的设计框架研究[J];计算机应用;2007年12期

10 吉顺慧;李必信;周宇;;基于顺序图的Web组合服务属性验证[J];东南大学学报(自然科学版);2011年02期

相关会议论文 前7条

1 张宇;方滨兴;张宏莉;;Internet拓扑演化机理验证[A];2008通信理论与技术新发展——第十三届全国青年通信学术会议论文集（下）[C];2008年

2 蔡元沛;邢薇;沙宁;;面向RIA的离线并发控制的研究[A];黑龙江省计算机学会2009年学术交流年会论文集[C];2010年

3 李磊;谭庆平;;Web服务兼容性及其验证算法[A];中国通信学会第六届学术年会论文集（上）[C];2009年

4 文静华;张梅;张焕国;;电子支付协议的博弈逻辑模型与形式化分析[A];2007年全国开放式分布与并行计算机学术会议论文集(上册)[C];2007年

5 王美姣;钱彦军;姚绍文;余正祥;;服务组合语言在SOA中的应用[A];云南省机械工程学会2010年年会论文集[C];2010年

6 吴亮;袁兆山;;基于模糊Petri网的语义Web服务组合[A];全国第20届计算机技术与应用学术会议（CACIS·2009）暨全国第1届安全关键技术与应用学术会议论文集（上册）[C];2009年

7 王小梅;李新明;刘东;韩星晔;;基于Petri网的网络传输协议建模与性能分析[A];全国第4届信号和智能信息处理与应用学术会议论文集[C];2010年

相关重要报纸文章 前1条

1 子文;ADIC StorNext/SAN存储海量数据[N];通信产业报;2003年

相关博士学位论文 前7条

1 许可;网格服务流的状态π演算形式化验证技术研究与应用[D];清华大学;2007年

2 龙慧云;基于进程代数的Web服务数据和组合的形式化方法研究[D];贵州大学;2009年

3 王玉英;基于赋时有色Petri网的Web服务组合建模验证与测试技术研究[D];西安电子科技大学;2012年

4 陈靖;带实时的传值与移动系统研究[D];中国科学院研究生院（软件研究所）;2003年

5 包力;Web服务组合形式化建模与验证研究[D];大连海事大学;2009年

6 胡佳;语义Web服务自动组合及验证的研究[D];天津大学;2010年

7 吴娴;基于策略域的分布式访问控制模型[D];苏州大学;2009年

相关硕士学位论文 前10条

1 张健;MMORPG服务器关键技术研究[D];浙江大学;2006年

2 付兴尊;基于进程代数的多路访问协议模型研究与实现[D];华东师范大学;2010年

3 刘子乾;基于攻击模式的系统漏洞检测工具的设计与实现[D];天津大学;2008年

4 卢建军;Web服务自动迁移[D];北京邮电大学;2006年

5 刘贤;基于工作流的Web服务组合建模研究[D];中南大学;2010年

6 朱晓红;基于状态演算的网格服务自动组合技术研究[D];重庆大学;2006年

7 吴铮;基于Pi演算的SOAP安全性分析与验证[D];中国石油大学;2008年

8 刘勇;有限PI演算的Petri网语义转换研究[D];吉林大学;2009年

9 张帆;基于异步π-演算的两阶段提交协议的形式化描述和验证[D];国防科学技术大学;2006年

10 康智辉;基于属性的层次移动IPv6（HMIPv6）协议的验证[D];内蒙古大学;2011年

本文编号：2017156