检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

适用于形式化验证的断言优化方法

中国电子科学研究院学报 2023年第2期18卷 166-175,188页

作者：李东方刘诗宇王纪王志昊闫皓中国航天科工集团第二研究院706所北京100854

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响... 详细信息

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系。在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性。

关键词：断言优化形式化验证状态空间爆炸影响锥模型长序列模型

在线全文

学校读者我要写书评

暂无评论

HDLC IP核的形式化验证

中国电子科学研究院学报 2022年第11期17卷 1078-1086页

作者：李东方刘诗宇王志昊王纪宋小敬沈炜中国航天科工集团第二研究院706所北京100854

目前,高级数据链路控制(High-Level Data Link Control, HDLC)协议控制器在航天型号中依然应用广泛,通常以IP核的形式被集成在通信部件中。但是近年,多个经过仿真验证的HDLC IP核在航天型号运行过程中出现了触发概率极小的功能错误,导... 详细信息

目前,高级数据链路控制(High-Level Data Link Control, HDLC)协议控制器在航天型号中依然应用广泛,通常以IP核的形式被集成在通信部件中。但是近年,多个经过仿真验证的HDLC IP核在航天型号运行过程中出现了触发概率极小的功能错误,导致数据帧丢失、通信功能失效甚至任务失败。在仅依靠仿真无法保证验证充分性的背景下,采用形式化验证方法进行功能验证。本文依据HDLC国际标准分析同步传输模式关键功能,将关键功能拆分为属性描述,并根据属性编写断言,从而建立HDLC协议同步传输模式关键功能用例集,并以正在航天型号中使用的某HDLC IP核为例,使用形式化验证工具进行验证实验,发现了此前从未发现的两处设计缺陷。针对这些设计缺陷,分析了其触发原理和可能造成的危害。

关键词：功能验证形式化验证 IP核 HDLC协议控制器

在线全文

学校读者我要写书评

暂无评论

基于手动/半自动装配线智能管控方法研究

航空制造技术 2022年第7期65卷 64-69页

作者：赵霖于成龙王崑声赵滟王家胜中国航天系统科学与工程研究院北京100048 中国航天科工集团第二研究院706所北京100854

为提升基于手动/半自动传统装配模式为主的航天产品装配效率,满足当前快速发展的航天产品研制生产需求,提出了传统模式下航天车间装配线智能管控的体系架构,讨论了装配信息建模、装配关联关系分析、装配进度演化预测、装配智能决策排产... 详细信息

为提升基于手动/半自动传统装配模式为主的航天产品装配效率,满足当前快速发展的航天产品研制生产需求,提出了传统模式下航天车间装配线智能管控的体系架构,讨论了装配信息建模、装配关联关系分析、装配进度演化预测、装配智能决策排产等主要内容;详细阐述了基于历史数据及数据分析挖掘算法进行工艺规程生成和工序工时计算的基本方法,探讨了基于装配实时状态的生产进度演化预测、决策及优化排产等技术,初步形成了以手动/半自动为主的航天车间装配生产线智能管控方法,对于后续进一步研究智能管控方法涉及的具体技术和实现方式、开发软件系统和提升装配管控能力具有一定的参考价值。

关键词：离散制造手动半自动装配线排产智能管控

基于关联分类的FPGA缺陷检测水平量化方法

在线全文

学校读者我要写书评

暂无评论

计算机工程与设计 2019年第7期40卷 1872-1877页

作者：王志昊冯志华中国航天科工集团第二研究院706所

为客观、全面地量化FPGA缺陷检测水平,并以此实现FPGA测试方检测水平比对,在统一的缺陷分类标准基础上,对面向FPGA缺陷的关联分类技术进行研究,借此建立不同项目间统一的水平量化标准,结合马尔科夫链理论,研究针对检测水平变化趋势的分... 详细信息

为客观、全面地量化FPGA缺陷检测水平,并以此实现FPGA测试方检测水平比对,在统一的缺陷分类标准基础上,对面向FPGA缺陷的关联分类技术进行研究,借此建立不同项目间统一的水平量化标准,结合马尔科夫链理论,研究针对检测水平变化趋势的分析方法,给出稳定水平量化方法。结合实例,阐述应用该方法的一般步骤,结果验证了该方法在FPGA缺陷检测水平的量化与对比工作上的可行性与有效性。

关键词：现场可编程门阵列缺陷检测缺陷分类关联规则马尔科夫链

在线全文

学校读者我要写书评

暂无评论

大力弘扬“两弹一星”精神

红旗文稿 2022年第5期 38-40页

作者：马杰中国航天科工集团第二研究院党委

党的十八大以来,习近平总书记多次谈到“两弹一星”精神及其时代价值。2020年4月23日,在第五个“中国航天日”和“东方红一号”卫星成功发射50周年到来之际,习近平总书记在给参与“东方红一号”任务的老科学家的回信中写道:“新时代的... 详细信息

党的十八大以来,习近平总书记多次谈到“两弹一星”精神及其时代价值。2020年4月23日,在第五个“中国航天日”和“东方红一号”卫星成功发射50周年到来之际,习近平总书记在给参与“东方红一号”任务的老科学家的回信中写道:“新时代的航天工作者要以老一代航天人为榜样,大力弘扬‘两弹一星’精神,敢于战胜一切艰难险阻.

关键词：东方红一号两弹一星 “两弹一星”精神中国航天习近平总书记科学家

在线全文

学校读者我要写书评

暂无评论

基于BPMN的复杂网络指挥控制流程优化

计算机工程与设计 2019年第10期40卷 2914-2920页

作者：魏然江山杨芳中国航天科工集团第二研究院706所

为满足指挥控制流程对任务内容动态更改的需求,缩短流程执行周期,针对传统工作流中流程节点静态、固化的现状,分析并扩展基于业务流程建模语言的任务状态空间,提出对流程节点增加部分提交,实现流程任务的最大化并行执行,研究增加任务状... 详细信息

为满足指挥控制流程对任务内容动态更改的需求,缩短流程执行周期,针对传统工作流中流程节点静态、固化的现状,分析并扩展基于业务流程建模语言的任务状态空间,提出对流程节点增加部分提交,实现流程任务的最大化并行执行,研究增加任务状态与流程核心业务逻辑间的耦合关系,保证流程的正确性和可靠性,提出通过对流程节点状态持续监控,实现动态控制的优化算法。通过对扩展后业务流程处理时间、完成效率等分析,验证使用扩展的BPMN语言可有效缩短指挥控制流程处理时间,提升流程的并行性和动态性。

关键词：指挥控制业务流程建模语言工作流复杂网络部分提交

在线全文

学校读者我要写书评

暂无评论

基于国产处理器的视频记录重演系统设计实现

计算机工程与设计 2019年第11期40卷 3349-3356页

作者：张力詹承华中国航天科工集团第二研究院706所

为提高战场指挥控制的时效性和准确性,开展车载武器系统的控制信号采集、编码压缩和记录存储的机理分析,提出一种基于国产处理器的战场态势记录重演系统架构,设计并实现视频编解码服务器硬件电路及软件框架协议。设计解码客户端软件,通... 详细信息

为提高战场指挥控制的时效性和准确性,开展车载武器系统的控制信号采集、编码压缩和记录存储的机理分析,提出一种基于国产处理器的战场态势记录重演系统架构,设计并实现视频编解码服务器硬件电路及软件框架协议。设计解码客户端软件,通过测试用例对系统的功能架构进行验证。实验结果表明,该系统可实时记录多路视频信号,按照时间戳序列化存储、形成索引。该系统对外提供标准的视频接口和网络接口,具有很强的移植性。

关键词：系统架构记录重演 H.264 国产处理器车载武器

在线全文

学校读者我要写书评

暂无评论

基于双ZYNQ平台的可信架构研究与实现

计算机工程与设计 2019年第7期40卷 1859-1865页

作者：张力詹承华杨林高淑敏中国航天科工集团第二研究院706所

分析现有嵌入式ZYNQ平台启动方式,结合可信度量和TCG信任链传递机制,在满足嵌入式系统启动实时性的前提下,设计两级流水线的可信启动方式。以专用TPM作为可信根源,度量上电启动的引导文件的完整性和真实性,建立一条嵌入式平台从上电到... 详细信息

分析现有嵌入式ZYNQ平台启动方式,结合可信度量和TCG信任链传递机制,在满足嵌入式系统启动实时性的前提下,设计两级流水线的可信启动方式。以专用TPM作为可信根源,度量上电启动的引导文件的完整性和真实性,建立一条嵌入式平台从上电到内核启动的信任链,为应用提供可信的执行环境。实验结果表明,该方法能有效验证启动引导文件的完整性,最小限度增加时间开销,满足双ZYNQ平台的启动效率。

关键词：信任链双ZYNQ平台可信根度量启动技术

在线全文

学校读者我要写书评

暂无评论

飞行器可用实时以太网技术

计算机工程与设计 2019年第10期40卷 2813-2821页

作者：赵征帆丁传红中国航天科工集团第二研究院706所

为将实时以太网技术应用于飞行器通信系统,以改进飞行器设备间通信存在的多级总线并存、线缆复杂、灵活性差、传输速率低等问题,对飞行器通信系统的需求进行分析,对POWERLINK总线协议的机制、软硬件架构进行研究,通过在FPGA内部搭建以... 详细信息

为将实时以太网技术应用于飞行器通信系统,以改进飞行器设备间通信存在的多级总线并存、线缆复杂、灵活性差、传输速率低等问题,对飞行器通信系统的需求进行分析,对POWERLINK总线协议的机制、软硬件架构进行研究,通过在FPGA内部搭建以运行在软核之上的开源协议栈为核心的片上系统,阐述将POWERLINK应用于飞行器综合信息处理计算机外部通信的一般方案,通过实验验证了该技术的可用性,为飞行器实时以太网技术的研究和应用提供了参考。

关键词：飞行器实时以太网片上可编程系统嵌入式计算机总线技术通信网络