以DNA为载体的线性时序逻辑模型检测

发布时间：2017-07-17 11:31

  本文关键词：以DNA为载体的线性时序逻辑模型检测

  更多相关文章： 模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机

【摘要】：线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Logic,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.
【作者单位】： 郑州大学信息工程学院;
【关键词】： 模型检测 脱氧核糖核酸 线性时序逻辑 粘贴自动机
【基金】：国家自然科学基金(No.61250007,No.U1204608,No.U1304606,No.61572444) 中国博士后科学基金(No.2012M511588,No.2015M572120) 河南省高等学校青年骨干教师资助计划项目(No.2014GGJS-001)
【分类号】：TP301.1
【正文快照】： 1引言模型检测由图灵奖得主Clarke教授等人提出[1].它是一种能够自动验证系统是否满足给定性质的形式化核心方法与技术,被广泛地应用于硬件验证[2]、网络协议验证、安全协议验证[3]等领域.在时序逻辑模型检测中,线性时序逻辑[4](Linear Temporal Logic,LTL)、计算树逻辑[5](Co

【相似文献】

中国期刊全文数据库 前10条

1 戎玫;张广泉;;模型检测新技术研究[J];计算机科学;2003年05期

2 肖健宇;张德运;郑卫斌;;过程提取用于改善程序模型检测的可伸缩性[J];西安交通大学学报;2006年06期

3 袁志斌;徐正权;王能超;;软件模型检测中的抽象[J];计算机科学;2006年07期

4 刘吉锋;孙吉贵;;基于抽象-验证-细化范例的软件模型检测[J];计算机科学;2006年12期

5 化志章;吴传孙;揭安全;薛锦云;;软件模型检测新技术研究[J];微计算机信息;2007年36期

6 王飞明;胡元闯;董荣胜;;模型检测研究进展[J];广西科学院学报;2008年04期

7 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

8 何恺铎;顾明;宋晓宇;李力;李江;;面向源代码的软件模型检测及其实现[J];计算机科学;2009年01期

9 林璇;;模型检测方法在入侵检测中的应用研究[J];现代计算机(专业版);2009年02期

10 顾滨兵;;一种软件模型检测方法及其原型系统[J];微计算机应用;2010年11期

中国重要会议论文全文数据库 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

中国博士学位论文全文数据库 前10条

1 奚琪;基于模型检测的二进制代码恶意行为识别技术研究[D];解放军信息工程大学;2014年

2 江华;界程演算模型检测[D];贵州大学;2008年

3 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

4 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

5 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

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

7 尹良泽;基于SAT的组合迁移系统模型检测技术研究[D];清华大学;2014年

8 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

9 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

10 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

中国硕士学位论文全文数据库 前10条

1 李永亮;基于DNA计算的CTL模型检测方法研究[D];郑州大学;2015年

2 杨树峰;基于统计模型检测的无线传感器网络协议建模与分析[D];郑州大学;2015年

3 张兴兴;基于广义可能性测度的互模拟及CTL不动点语义[D];陕西师范大学;2015年

4 王彬;基于多值模型检测的SaaS应用测试及其自动化研究[D];陕西师范大学;2015年

5 王凯;基于模型检测多反例对软件进行调试[D];电子科技大学;2015年

6 邓楠轶;基于广义可能性测度的模型检测器GPoCheck的设计与实现[D];陕西师范大学;2015年

7 张恒;多值模型检测器的研究与实现[D];陕西师范大学;2015年

8 高毅;不同模型检测下信号并串转换模块功能建模的研究[D];电子科技大学;2014年

9 崔晓爽;基于GSTE模型检测的信号并串转换模块功能验证的研究[D];电子科技大学;2014年

10 许落汀;基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测及证据生成[D];华侨大学;2015年

，

本文编号：553425