期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
108
篇文章
<
1
2
…
6
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
面向参数化LTL的预测监控器构造技术
被引量:
6
1
作者
赵常智
董威
+1 位作者
隋平
齐治昌
《软件学报》
EI
CSCD
北大核心
2010年第2期318-333,共16页
介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的...
介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.
展开更多
关键词
运行时验证
软件监控
预测监控器
参数化
ltl
(linear
TEMPORAL
logic)
参数化Büchi自动机
下载PDF
职称材料
LTL公式到自动机的转换
被引量:
4
2
作者
郭建
边明明
韩俊岗
《计算机科学》
CSCD
北大核心
2008年第7期241-243,276,共4页
在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法。该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机。此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动...
在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法。该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机。此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换。
展开更多
关键词
模型检验
Buchi自动机
选择Buchi自动机
ltl
公式
下载PDF
职称材料
基于LTL Tableau的自动机构造
3
作者
刘万伟
王戟
陈火旺
《吉林大学学报(工学版)》
EI
CAS
CSCD
北大核心
2007年第1期132-135,共4页
基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(Stuffer Alternating Co-B&...
基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(Stuffer Alternating Co-Büchi)的具有线性复杂度的方法,该方法能够降低最终乘积自动机的空间复杂度。
展开更多
关键词
计算机软件
模型检验
ltl
TABLEAU
Co—Büchi自动机
下载PDF
职称材料
用LTL模型检验的方法验证SpaceWire检错机制
被引量:
7
4
作者
董玲玲
关永
+3 位作者
李晓娟
施智平
张杰
华伟
《计算机工程与应用》
CSCD
2012年第22期88-94,共7页
SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。...
SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑(LTL)模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑(CTL)验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。
展开更多
关键词
形式化验证
SpaceWire标准
模型检验
分支时态逻辑(CTL)
线性时态逻辑(
ltl
)
下载PDF
职称材料
Lorentz变换链(LTL)原理的证明
5
作者
王丽君
《松辽学刊(自然科学版)》
1996年第2期69-70,共2页
本文证明了Lorentz变换链(LTL)原理.
关键词
Lorentz变换链
ltl
原理
闵柯夫斯基空间
下载PDF
职称材料
一维取向LTL型分子筛荧光阵列的快速组装
6
作者
张斌兴
苏美慧
+4 位作者
马强
王政
韩乐
宋智
李山
《发光学报》
EI
CAS
CSCD
北大核心
2016年第11期1339-1345,共7页
通过有效控制合成液配比,合成出了形貌规则、结晶度高且具有不同长径比的LTL型分子筛晶粒。采用"瓶中造船法",在不同长径比的LTL型分子筛晶粒孔道中组装稀土有机配合物,制得LTL分子筛/Eu-TTA主-客体荧光材料。荧光光谱表征结...
通过有效控制合成液配比,合成出了形貌规则、结晶度高且具有不同长径比的LTL型分子筛晶粒。采用"瓶中造船法",在不同长径比的LTL型分子筛晶粒孔道中组装稀土有机配合物,制得LTL分子筛/Eu-TTA主-客体荧光材料。荧光光谱表征结果表明,在激发波长为350 nm时,长径比为0.2的LTL分子筛/Eu-TTA晶粒在617 nm处的5D0→7F2发光强度最大,而长径比为3的晶粒发光强度最小。最后,将长径比为0.2的LTL分子筛/Eu-TTA晶粒在PEI修饰的玻璃表面快速擦涂10 s后,就制得厘米尺寸的一维取向LTL型分子筛荧光阵列。SEM表征结果证实,该分子筛荧光阵列中几乎所有的LTL分子筛晶粒都沿着与底基表面垂直的c轴方向一维高密度、单层有序排列。在激发波长为365 nm时,该一维取向LTL分子筛荧光阵列发出鲜艳的红色荧光。
展开更多
关键词
ltl
型分子筛
手工擦涂
荧光阵列
稀土有机配合物
下载PDF
职称材料
一种利用非确定规划的LTL合成方法
7
作者
陆旭
于斌
+1 位作者
田聪
段振华
《软件学报》
EI
CSCD
北大核心
2022年第8期2769-2781,共13页
LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博...
LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博弈(two-player game)问题,博弈的双方是环境和控制器,该问题的解称为合成策略.近年来,有研究从理论角度讨论了LTL合成与非确定规划(non-deterministicplanning)的相关性.基于此,提出了一种新的利用非确定规划求解LTL合成问题的方法,并证明了方法的正确性和完备性.具体而言,首先获得LTL公式对应的Büchi自动机,结合二人博弈定义,将LTL合成问题转换为完全可观测的非确定规划模型;然后交由高效规划器求解.通过实验结果说明:与其他LTL合成方法相比,提出的基于规划的合成方法在解质量方面具有较大的优势,能够获得规模较小的合成策略.
展开更多
关键词
二人博弈
BÜCHI自动机
ltl
合成
非确定规划
下载PDF
职称材料
一种有效的基于LTL和Petri网的模型检测方法
被引量:
1
8
作者
张斌
罗贵明
王平
《计算机应用》
CSCD
北大核心
2006年第10期2490-2493,共4页
模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检...
模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。
展开更多
关键词
模型检测
线性时序逻辑
自动机
PETRI网
下载PDF
职称材料
基于符号执行和LTL公式重写的测试用例产生方法
被引量:
3
9
作者
陈冬火
刘全
《计算机研究与发展》
EI
CSCD
北大核心
2013年第12期2661-2675,共15页
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法...
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.
展开更多
关键词
测试用例自动产生
符号执行
公式重写
模型检验
线性时序逻辑
输入
输出符号变迁系统
下载PDF
职称材料
一种基于LTL性质的面向对象并发程序切片方法
被引量:
1
10
作者
戎玫
何志学
张广泉
《计算机应用》
CSCD
北大核心
2008年第5期1300-1302,1306,共4页
为了缩减程序验证的状态空间,针对面向对象程序的并发机制,定义了程序中存在的依赖关系,提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法。切片后的程序与原程序对待验证的LTL性质具有相同的可满足性,而...
为了缩减程序验证的状态空间,针对面向对象程序的并发机制,定义了程序中存在的依赖关系,提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法。切片后的程序与原程序对待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。
展开更多
关键词
程序切片
线性时序逻辑性质
并发程序
程序验证
下载PDF
职称材料
LTL性质的可监视性
11
作者
王伟芳
樊丽丽
+1 位作者
李宝凤
赵光峰
《唐山师范学院学报》
2021年第3期18-20,共3页
以LTL的语义和可监视的定义为依据,证明了LTL性质的可监视性,得到了φ1∪φ2可监视的几个充分条件,还证明了可监视性在∨,■,○下是封闭的,在∪下不是封闭的。
关键词
可监视
ltl
公式
模型检验
拓扑
下载PDF
职称材料
LTL概率模型检验工具的实现与优化
12
作者
林哲超
董威
《计算机工程与科学》
CSCD
北大核心
2017年第5期892-896,共5页
概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性...
概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题,通过对原有的LTL概率模型检验算法进行优化,实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。
展开更多
关键词
ltl
概率模型检验
优化
下载PDF
职称材料
基于LTL语义的可达性控制器合成工具
13
作者
景丽莎
项周坤
《计算机系统应用》
2016年第11期22-28,共7页
控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现....
控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法,以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展,该算法主要用于解决基于分支时序逻辑(CTL)的控制器合成.另外,我们实现了相关的控制器合成工具CTAV/TGA(Timed Gamed Automata),在实现的过程中,使用on-the-fly的方式,避免了穷尽状态空间,同时,通过使用zone和抽象,大大缩减了状态数目,使时空效率控制在可接受的范围内.
展开更多
关键词
时间博弈自动机
控制器合成
线性时序逻辑(
ltl
)
on-the-fly
符号化方法
下载PDF
职称材料
基于SPIN的LTL属性分解方法研究
被引量:
2
14
作者
贺志宏
曾庆凯
《计算机应用与软件》
CSCD
北大核心
2014年第7期43-46,65,共5页
提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模...
提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。
展开更多
关键词
线性时序逻辑属性
模型检测
属性分解
静态程序切片
下载PDF
职称材料
带时间约束的LTL性质的模型检测的实现
被引量:
2
15
作者
部德振
《计算机工程与设计》
CSCD
北大核心
2011年第2期564-567,共4页
针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束...
针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。
展开更多
关键词
时间自动机
模型检测
线性时序逻辑性质
时间约束
空性检测
下载PDF
职称材料
时间自动机的LTL性质模型检测研究
16
作者
彭云全
魏绪凯
李广元
《计算机仿真》
CSCD
北大核心
2009年第5期92-95,共4页
为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略...
为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略。采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题。与DTSp in等著名的模型检测工具进行了实验比较,取得了较好的实验结果。
展开更多
关键词
时间自动机
模型检测
线性时序逻辑性质
二叉决策图共享存储
下载PDF
职称材料
一种基于离散时间自动机的LTL性质检测工具
17
作者
张文亮
彭云全
《计算机仿真》
CSCD
2008年第4期80-83,共4页
模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点。目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的...
模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点。目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低。介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度。实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin。
展开更多
关键词
离散时间自动机
非空性检测
线性时序逻辑性质
下载PDF
职称材料
LTL在STP轨迹分析中的应用
被引量:
1
18
作者
李晗
《铁道通信信号》
2018年第8期4-6,共3页
应用线性时序逻辑(LTL)对无线调车机车信号和监控系统(STP)的运行日志进行轨迹分析,实现自动定位故障发生时间,从而提升系统维护工作的自动化程度。
关键词
线性时序逻辑
无线调车机车信号和监控
轨迹分析
运行日志
下载PDF
职称材料
基于LTL的UML状态图测试用例生成方法
19
作者
高莉
《安徽建筑大学学报》
2015年第2期75-78,共4页
测试用例的自动生成是软件测试研究的主要方向之一,针对软件开发过程中测试数据生成存在低效、无目的、冗余等问题,提出了基于UML状态模型图的面向对象类级测试用例生成方法,将UML状态图转换成相应的事件确定有限状态机,通过线性时序逻...
测试用例的自动生成是软件测试研究的主要方向之一,针对软件开发过程中测试数据生成存在低效、无目的、冗余等问题,提出了基于UML状态模型图的面向对象类级测试用例生成方法,将UML状态图转换成相应的事件确定有限状态机,通过线性时序逻辑的模型检测技术,验证有限状态机模型的正确性,实验结果表明,该方法能够在不降低迁移覆盖准则的情况下,生成数量少、针对性强的测试用例集。
展开更多
关键词
软件测试
测试用例生成
UML状态图
线性时序逻辑
下载PDF
职称材料
结合搜索空间划分和抽象进行LTL模型检测
被引量:
6
20
作者
蒲飞
张文辉
《中国科学(E辑)》
CSCD
北大核心
2007年第12期1504-1520,共17页
在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别...
在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.
展开更多
关键词
搜索空间划分
求精
抽象
ltl
模型检测
原文传递
题名
面向参数化LTL的预测监控器构造技术
被引量:
6
1
作者
赵常智
董威
隋平
齐治昌
机构
国防科学技术大学计算机学院
出处
《软件学报》
EI
CSCD
北大核心
2010年第2期318-333,共16页
基金
国家自然科学基金Nos.60673118
60725206
+2 种基金
60970035
90818024
60803042~~
文摘
介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的正确绑定(binding)和使用(using);另一方面给出参数化预测监控器的概念.它由静态和动态两部分组成,静态部分由参数化Büchi自动机表示,动态部分为当前状态处的变量赋值.在系统运行过程中,预测监控器基于静态部分的参数化Büchi自动机,以on-the-fly的方式在当前状态处动态地提取和绑定变量赋值,递进地验证当前程序运行是否满足指定的参数化性质规约.在该过程中,参数化监控器能够精确地识别被验证性质的最小好/坏前缀.
关键词
运行时验证
软件监控
预测监控器
参数化
ltl
(linear
TEMPORAL
logic)
参数化Büchi自动机
Keywords
runtime verification
software monitoring
anticipatory monitor
pararneterized
ltl
(linear temporal logic)
parameterized Biichi automata
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
LTL公式到自动机的转换
被引量:
4
2
作者
郭建
边明明
韩俊岗
机构
西安电子科技大学微电子学院
西安邮电学院计算机系
出处
《计算机科学》
CSCD
北大核心
2008年第7期241-243,276,共4页
基金
国家自然科学基金(NO.90607008)资助
陕西省教育厅项目(07JK373)资助
文摘
在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法。该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机。此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换。
关键词
模型检验
Buchi自动机
选择Buchi自动机
ltl
公式
Keywords
Model checking,Buchi automata, Alternating buchi automata, Linear temporal logic
分类号
TP301.1 [自动化与计算机技术—计算机系统结构]
TP311.13 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于LTL Tableau的自动机构造
3
作者
刘万伟
王戟
陈火旺
机构
国防科技大学计算机学院
出处
《吉林大学学报(工学版)》
EI
CAS
CSCD
北大核心
2007年第1期132-135,共4页
基金
'973'国家重点基础研究计划项目(2005CB321802)
国家自然科学基金重点资助项目(60233020)
+1 种基金
'863'国家高技术研究发展计划项目(005AA113130)
教育部新世纪优秀人才支持计划项目(NCET-04-0996)
文摘
基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(Stuffer Alternating Co-Büchi)的具有线性复杂度的方法,该方法能够降低最终乘积自动机的空间复杂度。
关键词
计算机软件
模型检验
ltl
TABLEAU
Co—Büchi自动机
Keywords
computer software
model checking
ltl
Tableau
Co-Büchi automata
分类号
TP301 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
用LTL模型检验的方法验证SpaceWire检错机制
被引量:
7
4
作者
董玲玲
关永
李晓娟
施智平
张杰
华伟
机构
首都师范大学高可靠嵌入式系统技术北京市工程研究中心
北京化工大学信息科学与技术学院
出处
《计算机工程与应用》
CSCD
2012年第22期88-94,共7页
基金
国际科技合作项目(No.2011DFG13000)
科技部国际科技合作项目(No.2010DFB10930)
+2 种基金
北京市教委科技发展项目经费资助(No.KZ201210028036)
北京自然科学基金(No.4122017)
国家自然科学基金(No.61170304)
文摘
SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑(LTL)模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑(CTL)验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。
关键词
形式化验证
SpaceWire标准
模型检验
分支时态逻辑(CTL)
线性时态逻辑(
ltl
)
Keywords
formal verification
SpaceWire standard
model checking
Computional Tree Logic (CTL)
Linear Temporal Logic (
ltl
)
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
Lorentz变换链(LTL)原理的证明
5
作者
王丽君
机构
四平师范学院
出处
《松辽学刊(自然科学版)》
1996年第2期69-70,共2页
文摘
本文证明了Lorentz变换链(LTL)原理.
关键词
Lorentz变换链
ltl
原理
闵柯夫斯基空间
Keywords
Lorentz transformations linking
ltl
theorem
分类号
O411.1 [理学—理论物理]
下载PDF
职称材料
题名
一维取向LTL型分子筛荧光阵列的快速组装
6
作者
张斌兴
苏美慧
马强
王政
韩乐
宋智
李山
机构
省部共建天然气转化国家重点实验室培育基地(宁夏大学)
宁夏大学化学化工学院
出处
《发光学报》
EI
CAS
CSCD
北大核心
2016年第11期1339-1345,共7页
基金
国家自然科学基金(21066011
21366026)资助项目
文摘
通过有效控制合成液配比,合成出了形貌规则、结晶度高且具有不同长径比的LTL型分子筛晶粒。采用"瓶中造船法",在不同长径比的LTL型分子筛晶粒孔道中组装稀土有机配合物,制得LTL分子筛/Eu-TTA主-客体荧光材料。荧光光谱表征结果表明,在激发波长为350 nm时,长径比为0.2的LTL分子筛/Eu-TTA晶粒在617 nm处的5D0→7F2发光强度最大,而长径比为3的晶粒发光强度最小。最后,将长径比为0.2的LTL分子筛/Eu-TTA晶粒在PEI修饰的玻璃表面快速擦涂10 s后,就制得厘米尺寸的一维取向LTL型分子筛荧光阵列。SEM表征结果证实,该分子筛荧光阵列中几乎所有的LTL分子筛晶粒都沿着与底基表面垂直的c轴方向一维高密度、单层有序排列。在激发波长为365 nm时,该一维取向LTL分子筛荧光阵列发出鲜艳的红色荧光。
关键词
ltl
型分子筛
手工擦涂
荧光阵列
稀土有机配合物
Keywords
zeolite
ltl
manual assembly
fluorescent array
organolanthanide complexes
分类号
O611.4 [理学—无机化学]
下载PDF
职称材料
题名
一种利用非确定规划的LTL合成方法
7
作者
陆旭
于斌
田聪
段振华
机构
西安电子科技大学计算机科学与技术学院
综合业务网理论及关键技术国家重点实验室(西安电子科技大学)
出处
《软件学报》
EI
CSCD
北大核心
2022年第8期2769-2781,共13页
基金
国家自然科学基金(61806158,61732013,62172322,62002290)
中国博士后科学基金(2019T120881,2018M643585)
+2 种基金
国家重点研发计划(2018AAA0103202)
陕西省重点科技创新团队(2019TD-001)
陕西省自然科学基础研究计划(2021JQ-208)。
文摘
LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博弈(two-player game)问题,博弈的双方是环境和控制器,该问题的解称为合成策略.近年来,有研究从理论角度讨论了LTL合成与非确定规划(non-deterministicplanning)的相关性.基于此,提出了一种新的利用非确定规划求解LTL合成问题的方法,并证明了方法的正确性和完备性.具体而言,首先获得LTL公式对应的Büchi自动机,结合二人博弈定义,将LTL合成问题转换为完全可观测的非确定规划模型;然后交由高效规划器求解.通过实验结果说明:与其他LTL合成方法相比,提出的基于规划的合成方法在解质量方面具有较大的优势,能够获得规模较小的合成策略.
关键词
二人博弈
BÜCHI自动机
ltl
合成
非确定规划
Keywords
two-player game
Büchi automata
ltl
synthesis
non-deterministic planning
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
一种有效的基于LTL和Petri网的模型检测方法
被引量:
1
8
作者
张斌
罗贵明
王平
机构
清华大学软件学院
沈阳军区装备部
出处
《计算机应用》
CSCD
北大核心
2006年第10期2490-2493,共4页
基金
国家973规划项目(2004CB719400)
国家自然科学基金(60474026)
清华大学基础基金资助
文摘
模型检测的一个主要方法是构建线性与时序逻辑(LTL)公式φ的否定形式等价的B櫣chi自动机Aφ和系统模型M的正交积,并检测正交积的可接受语言是否为空。通过对GeneralizedB櫣chi自动机进行化简,可以减小自动机的状态空间,从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包,可以有效地对基于Petri网表示的系统模型进行模型检测。
关键词
模型检测
线性时序逻辑
自动机
PETRI网
Keywords
model checking
Linear Temporal Logic(
ltl
)
automata
Petri net
分类号
TP311.13 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于符号执行和LTL公式重写的测试用例产生方法
被引量:
3
9
作者
陈冬火
刘全
机构
苏州大学计算机科学与技术学院
计算机软件新技术国家重点实验室(南京大学)
符号计算与知识工程教育部重点实验室(吉林大学)
出处
《计算机研究与发展》
EI
CSCD
北大核心
2013年第12期2661-2675,共15页
基金
国家自然科学基金项目(61070223
61103045
+3 种基金
61070122
61272005
61303108)
江苏省自然科学基金项目(BK2012616)
文摘
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.
关键词
测试用例自动产生
符号执行
公式重写
模型检验
线性时序逻辑
输入
输出符号变迁系统
Keywords
auto-generation of test cases
symbolic execution
formula rewriting
model checking
linear temporal logic (
ltl
)
input/output symbolic transition system (IOSTS)
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
一种基于LTL性质的面向对象并发程序切片方法
被引量:
1
10
作者
戎玫
何志学
张广泉
机构
暨南大学深圳旅游学院
苏州大学计算机科学与技术学院
出处
《计算机应用》
CSCD
北大核心
2008年第5期1300-1302,1306,共4页
基金
江苏省高校自然科学研究项目(05KJB520119)
重庆市自然科学基金资助项目(2006BB2259)
文摘
为了缩减程序验证的状态空间,针对面向对象程序的并发机制,定义了程序中存在的依赖关系,提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法。切片后的程序与原程序对待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。
关键词
程序切片
线性时序逻辑性质
并发程序
程序验证
Keywords
program slicing
Linear Temporal Logic (
ltl
) property
concurrent program
program verification
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
LTL性质的可监视性
11
作者
王伟芳
樊丽丽
李宝凤
赵光峰
机构
唐山师范学院数学与计算科学学院
出处
《唐山师范学院学报》
2021年第3期18-20,共3页
基金
唐山师范学院科研基金项目(2016C12)。
文摘
以LTL的语义和可监视的定义为依据,证明了LTL性质的可监视性,得到了φ1∪φ2可监视的几个充分条件,还证明了可监视性在∨,■,○下是封闭的,在∪下不是封闭的。
关键词
可监视
ltl
公式
模型检验
拓扑
Keywords
monitorable
ltl
formula
model checking
topology
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
LTL概率模型检验工具的实现与优化
12
作者
林哲超
董威
机构
国防科学技术大学计算机学院
出处
《计算机工程与科学》
CSCD
北大核心
2017年第5期892-896,共5页
文摘
概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题,通过对原有的LTL概率模型检验算法进行优化,实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。
关键词
ltl
概率模型检验
优化
Keywords
ltl
probabilistic model checking
optimization
分类号
TP311.5 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于LTL语义的可达性控制器合成工具
13
作者
景丽莎
项周坤
机构
中国科学院软件研究所计算机科学国家重点实验室
中国科学院研究生院
苏州大学计算机学院
出处
《计算机系统应用》
2016年第11期22-28,共7页
文摘
控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法,以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展,该算法主要用于解决基于分支时序逻辑(CTL)的控制器合成.另外,我们实现了相关的控制器合成工具CTAV/TGA(Timed Gamed Automata),在实现的过程中,使用on-the-fly的方式,避免了穷尽状态空间,同时,通过使用zone和抽象,大大缩减了状态数目,使时空效率控制在可接受的范围内.
关键词
时间博弈自动机
控制器合成
线性时序逻辑(
ltl
)
on-the-fly
符号化方法
Keywords
timed game automata
controller synthesis
linear temporal logic(
ltl
)
on-the-fly
symbolic method
分类号
TP301.1 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于SPIN的LTL属性分解方法研究
被引量:
2
14
作者
贺志宏
曾庆凯
机构
南京大学计算机软件新技术国家重点实验室
南京大学计算机科学与技术系
出处
《计算机应用与软件》
CSCD
北大核心
2014年第7期43-46,65,共5页
基金
国家自然科学基金项目(61170070)
国家科技支撑计划项目(2012BAK26B01)
国家高技术研究发展计划项目(2011AA1A202)
文摘
提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。
关键词
线性时序逻辑属性
模型检测
属性分解
静态程序切片
Keywords
Linear temporal logic (
ltl
) property
Model checking
Property decomposition
Static program slicing
分类号
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
带时间约束的LTL性质的模型检测的实现
被引量:
2
15
作者
部德振
机构
中国科学院软件研究所计算机科学国家重点实验室
出处
《计算机工程与设计》
CSCD
北大核心
2011年第2期564-567,共4页
基金
国家自然科学基金项目(60673051
60736017
60873260)
文摘
针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。
关键词
时间自动机
模型检测
线性时序逻辑性质
时间约束
空性检测
Keywords
timed automata
model checking
ltl
property
clock constraint
emptiness checking
分类号
TP301.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
时间自动机的LTL性质模型检测研究
16
作者
彭云全
魏绪凯
李广元
机构
中国科学院软件研究所
中国科学院研究生院
出处
《计算机仿真》
CSCD
北大核心
2009年第5期92-95,共4页
基金
国家自然科学基金(60673051,60736017,60721061)
国家973计划资助(2002cb312200)
文摘
为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略。采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题。与DTSp in等著名的模型检测工具进行了实验比较,取得了较好的实验结果。
关键词
时间自动机
模型检测
线性时序逻辑性质
二叉决策图共享存储
Keywords
Timed automata
Model checking
ltl
property
Binary decision diagram
分类号
N945.12 [自然科学总论—系统科学]
下载PDF
职称材料
题名
一种基于离散时间自动机的LTL性质检测工具
17
作者
张文亮
彭云全
机构
中国科学院软件研究所计算机科学国家重点实验室
出处
《计算机仿真》
CSCD
2008年第4期80-83,共4页
基金
国家自然科学基金资助项目(60673051,60421001)
国家973计划资助项目(2002cb312200)
文摘
模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点。目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低。介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度。实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin。
关键词
离散时间自动机
非空性检测
线性时序逻辑性质
Keywords
Discrete timed automata
Non - emptiness checking
ltl
property
分类号
N945.12 [自然科学总论—系统科学]
下载PDF
职称材料
题名
LTL在STP轨迹分析中的应用
被引量:
1
18
作者
李晗
机构
中交机电工程局有限公司武汉技术中心
出处
《铁道通信信号》
2018年第8期4-6,共3页
文摘
应用线性时序逻辑(LTL)对无线调车机车信号和监控系统(STP)的运行日志进行轨迹分析,实现自动定位故障发生时间,从而提升系统维护工作的自动化程度。
关键词
线性时序逻辑
无线调车机车信号和监控
轨迹分析
运行日志
Keywords
ltl
STP
Trace analysis
Operation log
分类号
U284.48 [交通运输工程—交通信息工程及控制]
下载PDF
职称材料
题名
基于LTL的UML状态图测试用例生成方法
19
作者
高莉
机构
安徽建筑大学电子与信息工程学院计算机系
出处
《安徽建筑大学学报》
2015年第2期75-78,共4页
基金
国家科技支撑计划(2012BAJ08B00)
安徽高校省级自然科学研究重点项目(KJ2009A018Z)
校青年科研专项经费(201183-14)
文摘
测试用例的自动生成是软件测试研究的主要方向之一,针对软件开发过程中测试数据生成存在低效、无目的、冗余等问题,提出了基于UML状态模型图的面向对象类级测试用例生成方法,将UML状态图转换成相应的事件确定有限状态机,通过线性时序逻辑的模型检测技术,验证有限状态机模型的正确性,实验结果表明,该方法能够在不降低迁移覆盖准则的情况下,生成数量少、针对性强的测试用例集。
关键词
软件测试
测试用例生成
UML状态图
线性时序逻辑
Keywords
software testing
test case generation
UML state chart
ltl
分类号
TP31 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
结合搜索空间划分和抽象进行LTL模型检测
被引量:
6
20
作者
蒲飞
张文辉
机构
中国科学院软件所计算机科学国家重点实验室
出处
《中国科学(E辑)》
CSCD
北大核心
2007年第12期1504-1520,共17页
基金
国家自然科学基金(批准号:60573012
60421001)
国家重点基础研究发展规划(批准号:2002cb312200)资助项目
文摘
在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.
关键词
搜索空间划分
求精
抽象
ltl
模型检测
分类号
TP311.52 [自动化与计算机技术—计算机软件与理论]
原文传递
题名
作者
出处
发文年
被引量
操作
1
面向参数化LTL的预测监控器构造技术
赵常智
董威
隋平
齐治昌
《软件学报》
EI
CSCD
北大核心
2010
6
下载PDF
职称材料
2
LTL公式到自动机的转换
郭建
边明明
韩俊岗
《计算机科学》
CSCD
北大核心
2008
4
下载PDF
职称材料
3
基于LTL Tableau的自动机构造
刘万伟
王戟
陈火旺
《吉林大学学报(工学版)》
EI
CAS
CSCD
北大核心
2007
0
下载PDF
职称材料
4
用LTL模型检验的方法验证SpaceWire检错机制
董玲玲
关永
李晓娟
施智平
张杰
华伟
《计算机工程与应用》
CSCD
2012
7
下载PDF
职称材料
5
Lorentz变换链(LTL)原理的证明
王丽君
《松辽学刊(自然科学版)》
1996
0
下载PDF
职称材料
6
一维取向LTL型分子筛荧光阵列的快速组装
张斌兴
苏美慧
马强
王政
韩乐
宋智
李山
《发光学报》
EI
CAS
CSCD
北大核心
2016
0
下载PDF
职称材料
7
一种利用非确定规划的LTL合成方法
陆旭
于斌
田聪
段振华
《软件学报》
EI
CSCD
北大核心
2022
0
下载PDF
职称材料
8
一种有效的基于LTL和Petri网的模型检测方法
张斌
罗贵明
王平
《计算机应用》
CSCD
北大核心
2006
1
下载PDF
职称材料
9
基于符号执行和LTL公式重写的测试用例产生方法
陈冬火
刘全
《计算机研究与发展》
EI
CSCD
北大核心
2013
3
下载PDF
职称材料
10
一种基于LTL性质的面向对象并发程序切片方法
戎玫
何志学
张广泉
《计算机应用》
CSCD
北大核心
2008
1
下载PDF
职称材料
11
LTL性质的可监视性
王伟芳
樊丽丽
李宝凤
赵光峰
《唐山师范学院学报》
2021
0
下载PDF
职称材料
12
LTL概率模型检验工具的实现与优化
林哲超
董威
《计算机工程与科学》
CSCD
北大核心
2017
0
下载PDF
职称材料
13
基于LTL语义的可达性控制器合成工具
景丽莎
项周坤
《计算机系统应用》
2016
0
下载PDF
职称材料
14
基于SPIN的LTL属性分解方法研究
贺志宏
曾庆凯
《计算机应用与软件》
CSCD
北大核心
2014
2
下载PDF
职称材料
15
带时间约束的LTL性质的模型检测的实现
部德振
《计算机工程与设计》
CSCD
北大核心
2011
2
下载PDF
职称材料
16
时间自动机的LTL性质模型检测研究
彭云全
魏绪凯
李广元
《计算机仿真》
CSCD
北大核心
2009
0
下载PDF
职称材料
17
一种基于离散时间自动机的LTL性质检测工具
张文亮
彭云全
《计算机仿真》
CSCD
2008
0
下载PDF
职称材料
18
LTL在STP轨迹分析中的应用
李晗
《铁道通信信号》
2018
1
下载PDF
职称材料
19
基于LTL的UML状态图测试用例生成方法
高莉
《安徽建筑大学学报》
2015
0
下载PDF
职称材料
20
结合搜索空间划分和抽象进行LTL模型检测
蒲飞
张文辉
《中国科学(E辑)》
CSCD
北大核心
2007
6
原文传递
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
2
…
6
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部