吕正

作品数:7被引量:6H指数:2
导出分析报告
供职机构:西北大学更多>>
发文主题:多核处理器形式化建模确定有限自动机ARM处理器ARM更多>>
发文领域:自动化与计算机技术生物学更多>>
发文期刊:《微电子学与计算机》《西安交通大学学报》《计算机工程与应用》《计算机工程》更多>>
所获基金:国家高技术研究发展计划陕西省教育厅自然科学基金陕西省自然科学基金陕西省科技攻关计划更多>>
-

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
条 记 录,以下是1-7
视图:
排序:
一种ARM存储模型的快速检测方法被引量:2
《西安交通大学学报》2013年第6期68-72,共5页吕正 陈昊 陈峰 
国家"863计划"资助项目(2007AA01Z147)
针对ARM多核处理器存储模型正确性的快速检测问题,提出了一种利用时间序和悬空窗口的有界特性的快速检测方法,并实现了检测工具。该方法给出了ARM存储模型基于barrier的弱一致性模型的公理语义,通过定期扫描处理器的性能计数器获得访存...
关键词:ARM处理器 存储模型 正确性检测 
MOTEC:一个存储一致性模型验证工具被引量:1
《计算机工程》2012年第11期242-246,共5页吕正 陈昊 陈峰 吕毅 
国家"863"计划基金资助项目(2007AA01Z147)
由于缺乏可利用的额外观察条件,在芯片流片后阶段进行存储一致性模型验证较困难。为此,利用多核处理器系统中通用的性能计数器,通过定期扫描性能计数器以获得关键活动访存指令集合的信息,实现MOTEC工具。该工具由MOTEC随机指令发生模块...
关键词:多核处理器 存储一致性模型 形式验证 动态验证 存储系统 验证工具 
采用模型检测器的软件安全模型验证方法被引量:2
《西安交通大学学报》2011年第2期15-20,共6页陈峰 李伟华 陈昊 吕正 
国家自然科学基金资助项目(60803150;60803151);国家自然科学基金委员会-广东联合基金重点资助项目(U0835004);国家高技术研究发展计划资助项目(2008AA01Z411);陕西省自然科学基金资助项目(2009jm8012);陕西省教育厅自然科学专项资助项目(09JK736);陕西省科技攻关资助项目(2009k08-04)
针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型...
关键词:软件安全分析 确定有限自动机 形式化建模 模型检测 
机群文件系统共享语义测试方法
《计算机工程》2010年第10期76-79,共4页吕正 陈昊 吕毅 
国家"863"计划基金资助项目(2007AA01Z147)
机群文件系统能否满足用户需要的共享文件语义涉及机群文件系统服务的正确性、性能和易用性。为验证该类特性,提出文件系统共享语义测试概念,实现一个文件语义测试系统FSbench。FSbench使用随机测试和划分测试相结合的方法测试和验证文...
关键词:机群文件系统 文件共享语义 共享语义测试 软件测试 
模型检测MESIF Cache一致性协议被引量:1
《计算机工程与应用》2010年第17期66-68,152,共4页吕正 陈昊 陈峰 吕毅 
国家高技术研究发展计划(863) No.2007AA01Z147~~
在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂。Cache一致性协议的验证一直是模型检测在工业界主要应用之一,被工业界和学术界关注。相对传统方法而言,微结构...
关键词:模型检测 CACHE一致性协议 形式验证 
网格社区的进程代数模型(GCPAM)
《微电子学与计算机》2007年第8期95-98,共4页吕正 陈昊 
虚组织VO(VirtualOrganization)和网格社区概念是网格理论模型的一个重要组成部分,建立合适的网格社区理论模型有助于精确定义网格社区概念、研究网格社区的重要特性。借鉴进程代数的方法提出了网格社区进程代数模型(Grid Community Pro...
关键词:网格社区 进程代数 网格理论模型 
联网审计系统中审计分析模型的研究与应用
《中国高新技术企业》2007年第13期92-94,共3页林碧英 陈昊 吕正 孙雅娟 
计算机联网审计在实际审计中有着重要的应用。本文阐述了传统手工审计存在的问题及联网审计的优势,给出了联网审计的实现方法。在参考手工审计方法的基础上,给出了创建审计分析模型的方法。通过应用审计分析模型能够快速发现疑点数据,...
关键词:联网审计 疑点数据 审计分析模型 
检索报告 对象比较 聚类工具 使用帮助 返回顶部