李黎明

作品数：6被引量：22H指数：3
导出分析报告
供职机构：首都师范大学更多>>
发文主题：形式化验证定理证明SPACEWIRE形式化分析方法逻辑语言更多>>
发文领域：自动化与计算机技术电子电信更多>>
发文期刊：《首都师范大学学报（自然科学版）》《小型微型计算机系统》《软件学报》《计算机工程与设计》更多>>
所获基金：国家自然科学基金国际科技合作与交流专项项目北京市教委科学研究与科研基地建设项目北京市优秀人才培养资助更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-6
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
几何代数的高阶逻辑形式化被引量：5
《软件学报》2016年第3期497-516,共20页马莎 施智平 李黎明 关永 张杰 Xiaoyu SONG 
国家自然科学基金(61170304;61104035;61373034;61303014;61472468;61572331);国际科技合作计划(2010DFB10930;2011DFG13000);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)~~
几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法...
关键词：几何代数 形式化验证 定理证明 HOL-Light 几何积 
共形几何代数与机器人运动学的形式化被引量：3
《小型微型计算机系统》2016年第3期555-561,共7页马莎 施智平 关永 李黎明 邵振洲 张杰 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目;北京市属高校青年拔尖人才培育计划资助
共形几何代数作为一种新的几何表示和计算系统,它为经典几何提供了简洁、直观和统一的齐性代数框架,目前在现代科技的各个领域有很广泛的应用,但是利用共形几何代数进行计算和建模分析的传统方法如数值计算方法和符号方法存在计算不精...
关键词：共形几何代数 形式化验证 定理证明 HOL-Light 运动学反解 
结构建模法在硬件电路形式化验证中的应用被引量：1
《计算机工程与设计》2016年第1期259-263,共5页张杰 王亚丽 李黎明 李晓娟 
国家自然科学基金项目(61373034)
为解决硬件电路形式化验证过程中,验证对象的结构过于庞大复杂难以进行形式化描述与验证的问题,提出一种结构建模法。对两种不同的结构建模方法 (分解法和迭代法)分别进行讨论,分析两种方法的异同点以及适用性,详述结构建模过程中需要...
关键词：结构建模 形式化验证 定理证明 分解法 迭代法 74LS182 
SpaceWire译码电路在HOL4中的形式化验证被引量：5
《小型微型计算机系统》2013年第8期1959-1963,共5页张玉鹏 施智平 关永 李黎明 赵春娜 张杰 
国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035)资助;北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028036)资助;北京市优秀人才培养项目资助
SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成...
关键词：SpaceWire标准 形式化验证 定理证明 HOL 
嵌入式Linux与ARM环境下图像采集与显示被引量：2
《首都师范大学学报（自然科学版）》2013年第3期4-8,共5页底素然 李黎明 杨伟杰 张伟功 
SpaceWire是当前航天总线中的前沿技术,传输率大,可靠性高,可以作为构建我国新一代空间数据网络的选择.作为SpaceWire总线系统演示测试研究的一部分,本文基于嵌入式Linux系统与ARM的开发平台,利用CMOS摄像头仿真星载电子系统中的图像采...
关键词：SPACEWIRE Linux与ARM 数据采集与显示 CMOS摄像头 QT 
运用定理证明的形式化方法验证SpaceWire编码电路被引量：10
《小型微型计算机系统》2012年第6期1372-1376,共5页李黎明 关永 吴敏华 张杰 施智平 
国家自然科学基金项目(60873006;61070049;61170304)资助;国际科技合作项目(2010DFB10930)资助;北京市自然科学基金重点项目B类北京市教委科技发展重点项目资助
我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验...
关键词：形式化验证 SpaceWire标准 DS编码 定理证明 高阶逻辑 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部