国家重点基础研究发展计划(2010CB328102)

作品数：14被引量：21H指数：2
导出分析报告
相关作者：段振华王小兵黄伯虎聂鹏程杨琛更多>>
相关机构：西安电子科技大学武汉大学中国人民解放军69023部队中国空间技术研究院更多>>
相关期刊：《西安交通大学学报》《计算机研究与发展》《计算机学报》《西安电子科技大学学报》更多>>
相关主题：时序逻辑命题投影时序逻辑多核处理器并发SKYLINE算法更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
WISHBONE片上总线符号模型检测被引量：1
《计算机研究与发展》2014年第12期2759-2771,共13页逄涛 段振华 
国家"九七三"重点基础研究发展计划基金项目(2010CB328102);国家自然科学基金项目(61003078;61272117;61133001;61272118;91218301;61322202;61202038)
随着多核体系结构的出现和普及,片上总线逐渐成为影响片上系统功能和性能的关键部件.因此,片上总线的验证成为片上系统设计中一个重要组成部分.模型检测作为一种主流的形式化验证方法,可以自动化穷举搜索系统行为以决定片上系统的设计...
关键词：时序逻辑 符号模型检测 WISHBONE总线 片上系统 形式化验证 
PN2MSVL:工作流网到MSVL的转换
《计算机学报》2014年第12期2433-2442,共10页师亚 段振华 田聪 
国家"九七三"重点基础研究发展规划项目基金(2010CB328102);国家自然科学基金(61003078;61272117;61133001;61272118;91218301;61322202;61202038);综合业务网理论及关键技术国家重点实验室基金(ISN1102001)资助~~
现有的工作流网到程序设计语言的转换所生成的程序不仅可读性较差而且难以进行验证.针对这一情况,该文给出了一个工作流网到建模、仿真和验证语言(MSVL)的结构化转换工具PN2MSVL.该文首先定义了注释工作流网,然后以注释工作流网为中间模...
关键词：工作流网 建模 仿真 验证 转换 PETRI网 
扩展π演算对时间相关移动并发系统的建模与推演被引量：1
《西安交通大学学报》2014年第9期30-36,共7页罗玲 段振华 
国家"973"重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(61003078);综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001)
针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作...
关键词：Π演算 时间相关移动并发系统 形式化建模 推演 
性能非对称多核处理器上的自适应调度被引量：1
《计算机学报》2013年第4期773-781,共9页聂鹏程 段振华 田聪 杨孟飞 
国家"九七三"重点基础研究发展规划项目基金(2010CB328102);国家自然科学基金(61133001;61003078;61272117;61272118;61202038)资助~~
现有的性能非对称多核调度算法要么不能充分利用其体系结构而吞吐量低,要么能充分利用其体系结构但扩展性差.有些算法即使考虑了扩展性,但也局限于CPU核数目,没有考虑到任务数方面的扩展性.为了解决这些问题,作者提出了一个自适应调度算...
关键词：多核处理器 性能非对称 操作系统 调度 
真并发等价性下的流程模型转换方法
《西安交通大学学报》2012年第10期42-47,共6页张曼 段振华 
国家自然科学基金资助项目(60910004;61003078;61133001);国家重点基础研究发展规划资助项目(2010CB328102)
针对工作流建模过程中流程模型的演化问题,在真并发等价性概念下,提出将图形化控制流模型转换为顺序与并发结构可分隔处理的可分离形式的方法.采用自由选择工作流网建模控制流模型,以完全并发互模拟为真并发等价概念,定义两个安全网间...
关键词：工作流 PETRI网 自由选择工作流网 可分离工作流网 真并发等价 
进位保留加法器的命题投影时序逻辑组合验证被引量：2
《西安电子科技大学学报》2012年第5期192-196,共5页张南 段振华 
国家重点基础研究发展计划973资助项目(2010CB328102);国家自然科学基金资助项目(60910004;61133001;61003078;61202038;61272117);综合业务网国家重点实验室基金资助项目(ISN Lab Grant No.ISN1102001)
为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法.该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件...
关键词：时序逻辑 组合验证 进位保留加法器 超前进位加法器 
移动环境中的位置依赖连续轮廓查询被引量：2
《西安交通大学学报》2012年第6期79-86,共8页黄伯虎 张海宾 王小兵 刘旭东 
国家"973计划"资助项目(2010CB328102);国家自然科学基金资助项目(61003079);教育部高等学校博士学科点专项科研基金资助项目(20100203120012);中央高校基本科研业务费专项资金资助项目(K5051203003)
针对移动环境中查询点快速移动时连续、高效输出给定搜索区域数据轮廓的问题,提出一种位置依赖连续轮廓查询算法(LDCS).该算法结合数据流技术,首先使用R树快速更新查询数据,然后利用两次连续计算时搜索区域的重叠性构造被动数据流,并对...
关键词：数据流 位置服务 轮廓 查询处理 移动计算 
应用UML2.0模型的测试用例生成方法被引量：8
《西安交通大学学报》2011年第8期18-23,共6页张琛 段振华 
国家重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(60433010;60873018;60910004;91018010;61003078;61003079);教育部高等学校博士学科点专项科研基金资助项目(200807010012);中央高校基本科研业务费专项资金资助项目(JY10000903004)
针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证...
关键词：测试用例 命题投影时序逻辑 模型检测 覆盖准则 
基于枢轴选择策略的多核并行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公式表达的性质转换为性质自动机,...
关键词：时序逻辑 自动机 模型检测 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部