国家自然科学基金(60910004)

作品数：8被引量：8H指数：1
导出分析报告
相关作者：段振华杨琛王小兵聂鹏程黄伯虎更多>>
相关机构：西安电子科技大学武汉大学更多>>
相关期刊：《西安交通大学学报》《西安电子科技大学学报》《华中科技大学学报（自然科学版）》更多>>
相关主题：时序逻辑SKYLINE算法多核并行多核自动机更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
工作流网合成规则及其在流程设计中的应用被引量：1
《西安电子科技大学学报》2012年第2期200-206,共7页张曼 段振华 
国家自然科学基金资助项目(60910004,60873018,91018010,61003078,61003079,61133001);国家重点基础研究发展计划(973)资助项目(2010CB328102);综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对工作流网建模过程中节点精化方法只能扩展单节点的局限性,提出一种基于Petri网合成规则的工作流网精化方法.在活的和有界的自由选择网合成规则上添加限制,使其适用于自由选择工作流网的精化,定义可分离工作流网及其保持可分离性的...
关键词：工作流 PETRI网 合成规则 自由选择工作流网 可分离工作流网 
支持Stutter-不变性的命题区间时序逻辑
《西安电子科技大学学报》2011年第2期151-156,共6页杨琛 段振华 
国家自然科学基金重大国际合作项目资助项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展计划(973)资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项基金资助项目(JY10000903004)
为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,...
关键词：模型检测 时序逻辑 状态爆炸 
基于枢轴选择策略的多核并行skyline算法
《四川大学学报（工程科学版）》2011年第1期109-115,共7页黄伯虎 张海宾 逄涛 聂鹏程 
国家重点基础研究发展计划资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004JY10000903014)
针对当前大规模高维数据集skyline计算效率较低的问题,提出了一种多核并行算法MPSSI(Multi-core Par-allel Skyline computation based on Sorting and Incomparability)。首先对数据集进行预排序处理,简化了后续计算过程;并通过精心选...
关键词：SKYLINE计算 多核 并行算法 排序 信息检索 
PPTL模型检测器实现的一个关键技术被引量：3
《西安交通大学学报》2010年第10期24-29,共6页杨琛 段振华 
国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,...
关键词：时序逻辑 自动机 模型检测 
一种采用预排序策略的多核并行skyline算法
《华中科技大学学报（自然科学版）》2010年第10期31-34,共4页黄伯虎 段振华 张金磊 聂鹏程 
国家重点基础研究发展计划资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004;JY10000903014)
为提升大规模多维数据集的skyline计算效率,提出了一种多核并行算法MPSCS(multi-core parallelskyline computation based on sorting).首先按照任意一维对数据集进行预排序,然后划分为多个子集,使用skeleton并行程序设计模型进行并行...
关键词：并行算法 SKYLINE算法 并行编程 多核 预排序 
面向命题投影时序逻辑的安全协议模型检测被引量：1
《西安交通大学学报》2010年第8期30-35,共6页杨琛 段振华 王小兵 
国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望...
关键词：模型检测 协议验证 时序逻辑 安全协议 
框架时序逻辑语言MSVL中面向对象机制的实现被引量：1
《西安电子科技大学学报》2010年第3期559-564,575,共7页王小兵 段振华 
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金重大国际合作资助项目(60910004);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);陕西省科技攻关计划资助项目(2009K01-36);中央高校基本科研业务费专项资金资助项目(JY10000903004;JY10000903014)
针对目前时序逻辑语言存在框架问题、缺少面向对象机制、形式化程度过高等不足,提出了框架时序逻辑语言MSVL,包含新的框架操作符、等待语句和非确定的选择语句等技术,并且能够支持面向对象的程序设计.基于正则形和正则图,给出了MSVL解...
关键词：框架 时序逻辑 时序逻辑语言 面向对象程序设计 解释器 
利用投影时序逻辑的多内核进程调度建模与验证被引量：2
《西安交通大学学报》2010年第3期52-57,共6页舒新峰 段振华 
国家自然科学基金资助重大国际合作项目(60910004);国家"973计划"重点资助项目(2010CB328102);国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);总装备部预研项目(51315050105)
针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公...
关键词：投影时序逻辑 进程调度 定理证明 多核处理器 调度验证 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部