TA的每日心情 | 开心 2020-7-31 15:46 |
---|
签到天数: 1 天 [LV.1]初来乍到
|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
摘要:线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证
+ R& }, N8 [7 T7 M、安全协议验证等领域.然而到( D* p8 E8 @$ z d
目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear'Temporal Logic ,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机( Finite State Automata ,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.
6 U2 [: q! {, k6 E; I: Z1 q* j关键词:模型检测;脱氧核糖核酸;线性时序逻辑;粘贴自动机
8 a: L9 d! c: k! C* r3 s( w
以DNA为载体的线性时序逻辑模型检测.pdf
(948.09 KB, 下载次数: 0)
8 q3 {- a- s. K
) j% {$ b/ p. N' Z& M
|
|