李勇坚

作品数：5被引量：8H指数：2
导出分析报告
供职机构：中国科学院软件研究所更多>>
发文主题：VERILOG语义研究VERILOG语言操作语义形式化验证更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《小型微型计算机系统》《软件学报》《电子产品世界》更多>>
所获基金：国际科技合作与交流专项项目国家自然科学基金北京市教委科学研究与科研基地建设项目北京市优秀人才培养资助更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于学习的缓存一致性协议带参验证
《电子产品世界》2019年第1期82-83,87,共3页李勇坚 
0引言带参系统存在于许多应用领域中,比如缓存一致协议等。因为它的研究价值,验证这样的系统也就吸引来了形式化验证、模型检测和定理证明等社区的关注。要想验证带参系统的正确性,就必须验证任意实例大小的系统中的正确性,而这被证明...
关键词：形式化验证 一致性协议 缓存 定理证明 一致协议 模型检测 系统 
ROS中XML-RPC协议实现的形式化验证被引量：3
《小型微型计算机系统》2015年第12期2629-2633,共5页贾娟娟 施智平 关永 李勇坚 魏洪兴 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目资助;北京市属高校青年拔尖人才培育计划项目资助
XML-RPC协议是ROS节点通讯的核心调用机制,其实现的正确性关乎整个系统的顺利运行.使用模型检测和定理证明结合的方法对ROS系统中的XML-RPC协议进行验证.首先使用CBMC模型检测工具逐个验证协议源代码的函数,然后对模型检测不能全面验证...
关键词：ROS系统 XML-RPC协议 有界模型检测 定理证明 CBMC 
Verilog代数语义研究被引量：1
《软件学报》2003年第3期317-327,共11页李勇坚 何积丰 孙永强 
Supported by the DTfRTS (Design Techniques for Real-Time Hybrid Systems) Project of the International Institute for Software Technology; United Nations University (澳门联合国大学国际软件技术研究所实时混成系统的研究技术研究计划)
给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互...
关键词：代数语义 VERILOG语言 并发程序语义 程序设计语言 范式规约 
Verilog操作语义研究被引量：4
《软件学报》2002年第10期2021-2030,共10页李勇坚 何积丰 孙永强 
澳门联合国大学国际软件技术研究所"实时混成系统的研究技术"(Design Techniques for Real-Time Hybrid Systems)研究计划的资助项目~
提出了一个结构化操作语义模型,用于描述Verilog核心子集的语言特征,此子集包含了事件驱动、基于共享变量的并发特性、时间延迟等Verilog的主要语言成分.在此操作语义模型中,所有的Verilog程序将被统一地认为是开放式系统,所以在此操作...
关键词：VERILOG语言 操作语义 事件调度 观察模型 互模拟 同余性 
Verilog语言形式化语义研究
《软件学报》2001年第10期1573-1580,共8页李勇坚 孙永强 何积丰 
澳门联合国大学国际软件研究所资助项目~~
在连续离散混合时间模型中考虑 Verilog的语义行为 ,将混合模型中的一个区间作为 Verilog程序一次运行过程的指称 .提出了一种扩展的 ITL来描述这种混合区间 ,从而给出 Verilog的形式语义 .这种语义定义不仅考虑到了各种语言成分的最终...
关键词：VERILOG语言 形式化语义 硬件描述语言 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部