期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
8
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
PSL的有界模型检验
被引量:
2
1
作者
虞蕾
赵宗涛
《电子学报》
EI
CAS
CSCD
北大核心
2009年第3期614-621,共8页
基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性...
基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.
展开更多
关键词
PSL(property
specification
language)
有界模型检验
(bounded
model
checking
BMC)
SAT(propositional
satisfiability)
OBDD(ordered
binary
decision
diagram)
下载PDF
职称材料
一种改进的有界模型检验子句规则
被引量:
1
2
作者
尹文波
荆明娥
+1 位作者
周电
周晓方
《微电子学与计算机》
CSCD
北大核心
2007年第11期103-106,109,共5页
为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系...
为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句。实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。
展开更多
关键词
可满足性问题
有界模型检验
子句规则
精简布尔电路
下载PDF
职称材料
中断驱动控制系统的有界模型检验技术
3
作者
周筱羽
顾斌
+1 位作者
赵建华
杨孟飞
《软件学报》
EI
CSCD
北大核心
2015年第10期2485-2503,共19页
针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调...
针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.
展开更多
关键词
中断驱动系统
有界模型检验
超时检测
下载PDF
职称材料
有界模型检验综述
4
作者
于露
《电脑知识与技术(过刊)》
2017年第12X期70-71,共2页
无论是计算机系统硬件设计还是软件设计,随着设计规模越来越复杂和庞大,会产生越来越多的设计缺陷。传统检测方法代价高,并且难以检测这些设计缺陷。有界模型检验是一种重要的形式化验证方法,可以大大提高检测、验证的效率。作为一种形...
无论是计算机系统硬件设计还是软件设计,随着设计规模越来越复杂和庞大,会产生越来越多的设计缺陷。传统检测方法代价高,并且难以检测这些设计缺陷。有界模型检验是一种重要的形式化验证方法,可以大大提高检测、验证的效率。作为一种形式化方法构造系统的模拟运行过程,有界模型检验通过把有限状态机和线性时序逻辑验证规范否定形式编码成布尔可满足性实例,再由各种布尔可满足性工具来求解,以获得反例。由于有界模型检验使用深度优先搜索,它可以很快找到路径最短的反例。
展开更多
关键词
有界模型检验
模型
检验
SAT
下载PDF
职称材料
基于有界限模型检验的服务建模与自动组合
被引量:
1
5
作者
李艳
刘金江
《计算机工程与设计》
CSCD
北大核心
2011年第12期4079-4082,共4页
针对面向服务架构(SOA)体系的Web服务数量快速增长现状,为实现大规模服务场景下高效自动组合Web服务来满足用户复杂需求问题,提出一种基于有界模型检验的Web服务组合方法。其中,Web服务被建模为有限状态自动机,众多Web服务构成服务社区,...
针对面向服务架构(SOA)体系的Web服务数量快速增长现状,为实现大规模服务场景下高效自动组合Web服务来满足用户复杂需求问题,提出一种基于有界模型检验的Web服务组合方法。其中,Web服务被建模为有限状态自动机,众多Web服务构成服务社区,Web服务组合需求由线性时态逻辑公式描述,通过有界模型检验器的系统化搜索,该方法能够从服务社区中自动地构建满足需求的Web服务组合。实验结果表明,该方法能够适应较大规模的Web服务组合场景。
展开更多
关键词
有界模型检验
WEB服务组合
线性时态逻辑
服务社区
有限状态自动机
下载PDF
职称材料
龙芯2号微处理器浮点除法功能部件的形式验证
被引量:
3
6
作者
陈云霁
马麟
+1 位作者
沈海华
胡伟武
《计算机研究与发展》
EI
CSCD
北大核心
2006年第10期1835-1841,共7页
基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长.而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路.提出了基...
基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长.而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路.提出了基于SAT的字级模型检验方法,该方法将CNF扩展为能混合布尔公式和数学公式的E-CNF用以表示设计和系统规范,并对有界模型检验工具和SAT求解器进行字级的扩展,使它们能分别生成和处理E-CNF.龙芯2号微处理器浮点除法功能部件验证同时采用了基于PHDD和基于SAT的字级模型检验方法.数据表明,基于SAT的字级模型检验方法能快速地发现运算电路中的设计缺陷.两种方法互为补充,在能完全验证设计的同时显著缩短了设计周期.
展开更多
关键词
形式验证
PHDD
字级
模型
检验
SAT
CNF
有界模型检验
下载PDF
职称材料
一种面向CPS的控制应用程序协同验证方法
被引量:
3
7
作者
张雨
董云卫
+1 位作者
冯文龙
黄梦醒
《软件学报》
EI
CSCD
北大核心
2017年第5期1144-1166,共23页
信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制...
信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性(safety)和活性(liveness)等属性要求,提出了对该模型进行形式化验证的算法:基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高了可验证系统的规模.另外,结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.
展开更多
关键词
信息-物理融合系统
嵌入式控制应用程序
自动机理论
协同验证
有界模型检验
下载PDF
职称材料
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化
8
作者
解定宝
周岳翔
+2 位作者
卜磊
王林章
李宣东
《中国科学:信息科学》
CSCD
北大核心
2017年第3期288-309,共22页
混成系统是一类同时具有离散和连续行为的复杂系统,被广泛应用于控制系统建模.针对其安全性需求,对不安全状态进行有界可达性验证,是保障系统安全的重要手段.然而,当前技术所能处理的问题规模和现实生活里的实际需要尚有一定的距离.特...
混成系统是一类同时具有离散和连续行为的复杂系统,被广泛应用于控制系统建模.针对其安全性需求,对不安全状态进行有界可达性验证,是保障系统安全的重要手段.然而,当前技术所能处理的问题规模和现实生活里的实际需要尚有一定的距离.特别是组合混成系统由于涉及到各个组件间的协作与同步,组合状态空间快速爆炸,对其进行验证具有极高的复杂性.为控制问题的复杂度,一种面向路径的可达性分析方法在前期工作中被提出用来对组合线性混成系统进行有界可达性分析.该方法通过依次枚举潜在路径并进行验证的方式,有效地提升了所能处理的问题规模.当面对复杂系统时,上述面向路径的检测方法将会因为待检测路径数量的急剧上升而使得验证效率大幅降低,这也是模型检验状态空间爆炸问题的一种体现.为解决此问题,本文提出了一种状态空间约减技术以加速验证过程.当一组路径被判定为不可行时,定位出导致其不可行的原因,得到一个组合不可行路径片段.由于包含同样片段的组合路径一定不可行,因此在后续的路径遍历里只需要枚举与检验不包含组合不可行路径片段的路径,从而大幅减少需要检验的路径数量.此外,为了有效地规避此类组合路径片段,我们设计了一种全新的基于SMT编码的有界图结构遍历方法.实验表明,该优化技术大幅地提升了面向路径有界可达性分析方法的性能,整体性能也超越了当前最先进的同类工具.
展开更多
关键词
混成系统
有界模型检验
可达性分析
组合线性混成自动机
可满足性
不可约不可解子集
原文传递
题名
PSL的有界模型检验
被引量:
2
1
作者
虞蕾
赵宗涛
机构
国防科学技术大学计算机学院博士后流动站
第二炮兵工程学院计算机系
出处
《电子学报》
EI
CAS
CSCD
北大核心
2009年第3期614-621,共8页
基金
国家高技术研究发展计划(863计划)课题(No.2007AA010301)
国家自然科学基金(No.60503032)
中国博士后科学基金(No.20080431401)
文摘
基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.
关键词
PSL(property
specification
language)
有界模型检验
(bounded
model
checking
BMC)
SAT(propositional
satisfiability)
OBDD(ordered
binary
decision
diagram)
Keywords
PSL(property specification language)
BMC(bounded model checking)
SAT(propositional satisfiability)
OB- DD(ordered binary decision diagram)
分类号
TP301 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
一种改进的有界模型检验子句规则
被引量:
1
2
作者
尹文波
荆明娥
周电
周晓方
机构
复旦大学专用集成电路与系统国家重点实验室
出处
《微电子学与计算机》
CSCD
北大核心
2007年第11期103-106,109,共5页
基金
国家自然科学基金项目(90207002)
国家"863"高技术研究发展计划(2003AA1Z1120
2004AA1Z1050)
文摘
为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句。实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。
关键词
可满足性问题
有界模型检验
子句规则
精简布尔电路
Keywords
satisilability(SAT)
bounded model checking
clause form
reduced Boolean circuits
分类号
TN47 [电子电信—微电子学与固体电子学]
下载PDF
职称材料
题名
中断驱动控制系统的有界模型检验技术
3
作者
周筱羽
顾斌
赵建华
杨孟飞
机构
计算机软件新技术国家重点实验室(南京大学)
南京大学软件学院
西北工业大学计算机学院
南京大学计算机科学与技术系
中国空间技术研究院
出处
《软件学报》
EI
CSCD
北大核心
2015年第10期2485-2503,共19页
基金
国家自然科学基金(91118007
61321491)
国家高技术研究发展计划(863)(2012AA011205)
文摘
针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.
关键词
中断驱动系统
有界模型检验
超时检测
Keywords
interrupt-driven system
bounded model checking
deadline detection
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
有界模型检验综述
4
作者
于露
机构
同济大学
出处
《电脑知识与技术(过刊)》
2017年第12X期70-71,共2页
文摘
无论是计算机系统硬件设计还是软件设计,随着设计规模越来越复杂和庞大,会产生越来越多的设计缺陷。传统检测方法代价高,并且难以检测这些设计缺陷。有界模型检验是一种重要的形式化验证方法,可以大大提高检测、验证的效率。作为一种形式化方法构造系统的模拟运行过程,有界模型检验通过把有限状态机和线性时序逻辑验证规范否定形式编码成布尔可满足性实例,再由各种布尔可满足性工具来求解,以获得反例。由于有界模型检验使用深度优先搜索,它可以很快找到路径最短的反例。
关键词
有界模型检验
模型
检验
SAT
分类号
TP306.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于有界限模型检验的服务建模与自动组合
被引量:
1
5
作者
李艳
刘金江
机构
山东理工大学计算机科学与技术学院
南阳师范学院计算机与信息技术学院
出处
《计算机工程与设计》
CSCD
北大核心
2011年第12期4079-4082,共4页
基金
河南省科技厅科技攻关基金项目(102102210483
102102210465)
河南省重大科技攻关基金项目(092102110274)
文摘
针对面向服务架构(SOA)体系的Web服务数量快速增长现状,为实现大规模服务场景下高效自动组合Web服务来满足用户复杂需求问题,提出一种基于有界模型检验的Web服务组合方法。其中,Web服务被建模为有限状态自动机,众多Web服务构成服务社区,Web服务组合需求由线性时态逻辑公式描述,通过有界模型检验器的系统化搜索,该方法能够从服务社区中自动地构建满足需求的Web服务组合。实验结果表明,该方法能够适应较大规模的Web服务组合场景。
关键词
有界模型检验
WEB服务组合
线性时态逻辑
服务社区
有限状态自动机
Keywords
bounded model checking
web service composition
liner temporary logic
service community
finite state machine
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
龙芯2号微处理器浮点除法功能部件的形式验证
被引量:
3
6
作者
陈云霁
马麟
沈海华
胡伟武
机构
中国科学院计算技术研究所微处理器研究中心
出处
《计算机研究与发展》
EI
CSCD
北大核心
2006年第10期1835-1841,共7页
基金
国家"九七三"重点基础研究发展规划基金项目(2005CB321600)
国家自然科学基金杰出青年基金项目(60325205)
+4 种基金
国家"八六三"高技术研究发展计划重点基金项目(2002AA110010
2005AA110010
2005AA119020)
中国科学院计算技术研究所基础研究基金项目(20056020)
中国科学院计算技术研究所知识创新课题基金项目(20056240)~~
文摘
基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长.而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路.提出了基于SAT的字级模型检验方法,该方法将CNF扩展为能混合布尔公式和数学公式的E-CNF用以表示设计和系统规范,并对有界模型检验工具和SAT求解器进行字级的扩展,使它们能分别生成和处理E-CNF.龙芯2号微处理器浮点除法功能部件验证同时采用了基于PHDD和基于SAT的字级模型检验方法.数据表明,基于SAT的字级模型检验方法能快速地发现运算电路中的设计缺陷.两种方法互为补充,在能完全验证设计的同时显著缩短了设计周期.
关键词
形式验证
PHDD
字级
模型
检验
SAT
CNF
有界模型检验
Keywords
formal verification
* PHDD
word level model checking
SAT CNF
bounded model checking
分类号
TP301 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
一种面向CPS的控制应用程序协同验证方法
被引量:
3
7
作者
张雨
董云卫
冯文龙
黄梦醒
机构
南海海洋资源利用国家重点实验室(海南大学)
海南大学信息科学技术学院
西北工业大学计算机学院
出处
《软件学报》
EI
CSCD
北大核心
2017年第5期1144-1166,共23页
基金
国家自然科学基金(61462022
61363071)
+6 种基金
国家科技支撑计划(2014BAD10B04
2015BAH55F04)
海南省重大科技计划(ZDKJ2016015)
海南省自然科学基金(614232
614220)
海南省产学研一体化专项(cxy20150025)
海南大学科研启动基金(kyqd1610)~~
文摘
信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性(safety)和活性(liveness)等属性要求,提出了对该模型进行形式化验证的算法:基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高了可验证系统的规模.另外,结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.
关键词
信息-物理融合系统
嵌入式控制应用程序
自动机理论
协同验证
有界模型检验
Keywords
cyber-physical system
embedded control software program
automata theoretic
co-verification
bounded model checking
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化
8
作者
解定宝
周岳翔
卜磊
王林章
李宣东
机构
南京大学计算机软件新技术国家重点实验室
江苏省软件新技术与产业化协同创新中心
出处
《中国科学:信息科学》
CSCD
北大核心
2017年第3期288-309,共22页
基金
国家重点基础研究发展计划(973)(批准号:2014CB340703)
国家自然科学基金(批准号:61561146394
+1 种基金
61572249
61321491)资助项目
文摘
混成系统是一类同时具有离散和连续行为的复杂系统,被广泛应用于控制系统建模.针对其安全性需求,对不安全状态进行有界可达性验证,是保障系统安全的重要手段.然而,当前技术所能处理的问题规模和现实生活里的实际需要尚有一定的距离.特别是组合混成系统由于涉及到各个组件间的协作与同步,组合状态空间快速爆炸,对其进行验证具有极高的复杂性.为控制问题的复杂度,一种面向路径的可达性分析方法在前期工作中被提出用来对组合线性混成系统进行有界可达性分析.该方法通过依次枚举潜在路径并进行验证的方式,有效地提升了所能处理的问题规模.当面对复杂系统时,上述面向路径的检测方法将会因为待检测路径数量的急剧上升而使得验证效率大幅降低,这也是模型检验状态空间爆炸问题的一种体现.为解决此问题,本文提出了一种状态空间约减技术以加速验证过程.当一组路径被判定为不可行时,定位出导致其不可行的原因,得到一个组合不可行路径片段.由于包含同样片段的组合路径一定不可行,因此在后续的路径遍历里只需要枚举与检验不包含组合不可行路径片段的路径,从而大幅减少需要检验的路径数量.此外,为了有效地规避此类组合路径片段,我们设计了一种全新的基于SMT编码的有界图结构遍历方法.实验表明,该优化技术大幅地提升了面向路径有界可达性分析方法的性能,整体性能也超越了当前最先进的同类工具.
关键词
混成系统
有界模型检验
可达性分析
组合线性混成自动机
可满足性
不可约不可解子集
Keywords
hybrid system
bounded model checking
reachability analysis
compositional linear hybrid automata
satisfiability modulo theories
irreducible infeasible subset
分类号
TP301.1 [自动化与计算机技术—计算机系统结构]
原文传递
题名
作者
出处
发文年
被引量
操作
1
PSL的有界模型检验
虞蕾
赵宗涛
《电子学报》
EI
CAS
CSCD
北大核心
2009
2
下载PDF
职称材料
2
一种改进的有界模型检验子句规则
尹文波
荆明娥
周电
周晓方
《微电子学与计算机》
CSCD
北大核心
2007
1
下载PDF
职称材料
3
中断驱动控制系统的有界模型检验技术
周筱羽
顾斌
赵建华
杨孟飞
《软件学报》
EI
CSCD
北大核心
2015
0
下载PDF
职称材料
4
有界模型检验综述
于露
《电脑知识与技术(过刊)》
2017
0
下载PDF
职称材料
5
基于有界限模型检验的服务建模与自动组合
李艳
刘金江
《计算机工程与设计》
CSCD
北大核心
2011
1
下载PDF
职称材料
6
龙芯2号微处理器浮点除法功能部件的形式验证
陈云霁
马麟
沈海华
胡伟武
《计算机研究与发展》
EI
CSCD
北大核心
2006
3
下载PDF
职称材料
7
一种面向CPS的控制应用程序协同验证方法
张雨
董云卫
冯文龙
黄梦醒
《软件学报》
EI
CSCD
北大核心
2017
3
下载PDF
职称材料
8
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化
解定宝
周岳翔
卜磊
王林章
李宣东
《中国科学:信息科学》
CSCD
北大核心
2017
0
原文传递
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部