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

doi:10.3969/j.issn.0372-2112.2016.06.001

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2025-07-02

- 以DNA为载体的线性时序逻辑模型检测
- Conduct Linear Temporal Logic Model Checking via DNA Molecules
- 电子学报 2016年44卷第6期页码：1265-1271
- 作者机构：
  
  郑州大学信息工程学院,河南,郑州,450001
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.61250007,No.U1204608,No.U1304606,No.61572444);中国博士后科学基金 (No.2012M511588,No.2015M572120);河南省高等学校青年骨干教师资助计划项目 (No.2014GGJS-001)
- DOI：10.3969/j.issn.0372-2112.2016.06.001
  中图分类号： TP301TP384
- 网络出版：2016-06-25，
  
  纸质出版：2016
- 稿件说明：
移动端阅览
以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016,44(6):1265-1271.

Conduct Linear Temporal Logic Model Checking via DNA Molecules[J]. Acta Electronica Sinica, 2016, 44(6): 1265-1271.
以DNA为载体的线性时序逻辑模型检测[J]. 电子学报, 2016,44(6):1265-1271. DOI： 10.3969/j.issn.0372-2112.2016.06.001.

Conduct Linear Temporal Logic Model Checking via DNA Molecules[J]. Acta Electronica Sinica, 2016, 44(6): 1265-1271. DOI： 10.3969/j.issn.0372-2112.2016.06.001.

摘要

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止

该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid

DNA)为载体对线性时序逻辑(Linear Temporal Logic

LTL)实施模型检测

给出了使用粘贴自动机实现Until算子模型检测的方法.首先

使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata

FSA)模型进行编码;然后

将系统模型转换为粘贴自动机的输入字符串;最后

用粘贴自动机验证系统是否满足公式.仿真实验结果证实

新方法可实现对LTL逻辑时序算子的检测.

Abstract

The linear temporal logic (LTL) model checking is widely used in processor design and verification

network protocol verification and security protocol verification.Up to now

this technique can only be realized on the platform of electronic computer.In order to conduct LTL model checking under the circumstance of deoxyribo nucleic acid (DNA)

we proposed a method to check the Until constructor via a sticker automaton.We encode a finite state automaton (FSA) which is a model of the formula Until

with a DNA sticker automaton.And we convert a model of a system into its paths

as the input strings of the sticker automaton.We verify whether the system satisfies the formula or not

by using the sticker automaton.In this way

the formula Until can be checked with the double strand DNA molecules.The simulation results show that the method can successfully check the basic temporal formulas.

关键词

Keywords

references

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

时间感知Web服务交互行为建模与失配检测方法研究

实时模型检测中基于驻留环的精确加速

基于XYZ/ADL的Web服务组合描述与验证

缓冲区溢出漏洞精确检测方法研究

面向SoC系统芯片中跨时钟域设计的模型检验方法