期刊导航
期刊开放获取
vip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
3
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
用LTL模型检验的方法验证SpaceWire检错机制
被引量：
7
1
作者
董玲玲
关永
+3 位作者
李晓娟
施智平
张杰
华伟
《计算机工程与应用》
CSCD
2012年第22期88-94,共7页
SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。...
SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑(LTL)模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑(CTL)验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。
展开更多
关键词
形式化验证
SpaceWire标准
模型检验
分支时态逻辑(
ctl
)
线性时态逻辑(
ltl
)
在线阅读
下载PDF
职称材料
基于ASP的CSP并发系统验证研究
被引量：
4
2
作者
赵岭忠
张超
钱俊彦
《计算机科学》
CSCD
北大核心
2012年第12期125-132,共8页
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为...
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。
展开更多
关键词
通信顺序进程
回答集编程
ltl
ctl
在线阅读
下载PDF
职称材料
时态逻辑描述能力比较研究
被引量：
1
3
作者
黎升洪
缪淮扣
《计算机工程与应用》
CSCD
北大核心
2006年第22期75-77,共3页
时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述...
时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述,对时态逻辑描述能力进行了比较。
展开更多
关键词
时态逻辑
模型检查
ctl
^＊
ltl
在线阅读
下载PDF
职称材料
题名
用LTL模型检验的方法验证SpaceWire检错机制
被引量：
7
1
作者
董玲玲
关永
李晓娟
施智平
张杰
华伟
机构
首都师范大学高可靠嵌入式系统技术北京市工程研究中心
北京化工大学信息科学与技术学院
出处
《计算机工程与应用》
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
职称材料
题名
基于ASP的CSP并发系统验证研究
被引量：
4
2
作者
赵岭忠
张超
钱俊彦
机构
桂林电子科技大学计算机科学与工程学院
出处
《计算机科学》
CSCD
北大核心
2012年第12期125-132,共8页
基金
国家自然科学基金(61063002)
广西自然基金(2011GXNSFA018166
+3 种基金
2011GXNSFA018164)
武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-06)
广西可信软件重点实验室基金项目(kx201113)
广西研究生教育创新计划项目(2010105950812M28)资助
文摘
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。
关键词
通信顺序进程
回答集编程
ltl
ctl
Keywords
Communicating sequential processes
Answer set program
ltl/ctl
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
时态逻辑描述能力比较研究
被引量：
1
3
作者
黎升洪
缪淮扣
机构
上海大学计算机工程与科学学院
出处
《计算机工程与应用》
CSCD
北大核心
2006年第22期75-77,共3页
基金
国家自然科学基金资助项目(编号:60373072)
江西省教育厅科技项目(赣教科技便函字[2002]01号)
文摘
时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述,对时态逻辑描述能力进行了比较。
关键词
时态逻辑
模型检查
ctl
^＊
ltl
Keywords
temporal logic,model checking,
ctl
^＊,
ltl
分类号
TP18 [自动化与计算机技术—控制理论与控制工程]
在线阅读
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
用LTL模型检验的方法验证SpaceWire检错机制
董玲玲
关永
李晓娟
施智平
张杰
华伟
《计算机工程与应用》
CSCD
2012
7
在线阅读
下载PDF
职称材料
2
基于ASP的CSP并发系统验证研究
赵岭忠
张超
钱俊彦
《计算机科学》
CSCD
北大核心
2012
4
在线阅读
下载PDF
职称材料
3
时态逻辑描述能力比较研究
黎升洪
缪淮扣
《计算机工程与应用》
CSCD
北大核心
2006
1
在线阅读
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
