基于NuSMV的AADL模型形式化验证技术

结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法，并给出验证属性的统计信息。     

工程师应该熟练掌握形位公差标准

六○六所近期对百余名助理工程师进行了晋升工程师的技术考核,专业知识的考试科目选择了形位公差标准。经过再次宣讲标准和集中复习、辅导,考了公差符号,公差带     

面向机载计算机的高级语言和汇编语言符号调试程序设计

符号调试程序,是一种支持用户在目标机上动态调试、跟踪源程序运行的的工具。本文描述的JDBG就是一个支持某高级语言和机载计算机汇编的符号调试程序,除介绍JDBG的功能、总体结构和部分功能的实現方法外,还详细地介绍了JDBG的设计特色,如支持多种语言源程序的调试、支持扩充存储器的使用、支持动态变量查看点、符号表的动态加载等。针对开发环境的特点,本文介绍的单步命令及动态变量查看点的实现方法也颇具特点。     

飞机液压系统机件故障分析法探讨

液压附件结构复杂、故障难找。液压附件有一些简单形象的标准符号，利用其符号可将一些集成化程度较高的附件概括出附件功能原理，绘制出符号原理图。在此基础上，拟定试验方法，查找故障原因，直观有效。     

《机械设计基础》网上考试系统的开发与研究

通过剖析传统《机械设计基础》考试方法存在的弊端，从考试系统的建立、系统的组成与开发、系统的使用与特点等方面介绍《机械设计基础》网上考试系统的设计思路，并综合分析了网上考试系统试题的生成、在线学习和系统维护等多种功能的实现从而发挥了网络资源在教学和管理中的优势。     

交叉符号调试程序设计

本文介绍了一个在Ｖａｘ计算机上实现的汇编级符号调试程序的设计思想和实现方法，并讨论了符号调试程序的一般设计原理。     

机载图形符号显示技术研究

针对机载显示软件中存在的图形符号显示与设备相关性强、编码量大、工程实践繁琐等问题，提出了一种新的开发方法，通过定义显示图元、将符号分解为具有不同参数图元集合的方法，脱离了具体平台的硬件约束，做到了符号显示与设备无关，并开发了专用图符生成工具，减少了显示模块设计的复杂度。     

中俄飞机飞行力学术语和符号对比

介绍、列出了中俄两国现行飞行力学标准；依据这些标准，对两国飞行力学方面的坐标轴系、术语、定义和符号进行了对比分析；指出两国的坐标轴系、术语、定义和符号体系基本相同，其间最大的差别是坐标轴的指向不同，从而造成一些参数的正负符号不同。     

基于符号序列联合熵的航空发动机健康监控方法

引入信息熵理论,结合对多参数时间序列的符号化处理,探讨其在航空发动机健康监控中的应用.利用符号序列联合熵对航空发动机性能参数无序程度的描述,分析航空发动机健康状态及其演化方向.对两组实际飞行数据的实验分析表明,该方法描述的航空发动机的健康发展趋势与实际情况相吻合,能够较好反映航空发动机的健康状态,可以为航空发动机的健康...     

计算机自动绘制发动机故障树技术的研究

介绍了用AutoCAD绘图软件建立绘制故障树所需图形库的方法，即将故障树中使用的事件符号和逻辑符号进行分类、组合，归纳为11种图元，供用户交互使用；调用图元时，可根据需要，进行移动、缩放、转角、编辑和修改等，以便在确定了系统的顶事件，中间件和底事件以后快速而方便地绘制故障树，这样，不仅可使故障树精确、清晰、美观，而且还可以进行优化与修改，提高绘制质量。     

汇编语言题库管理系统的设计与开发

本文是对汇编语言题库管理系统设计的详细说明,其重点是对试题库的维护设计的试卷生成算法的说明,其中在对试题库的维护设计介绍中,本文详细阐述了关于优化题库结构设计的一些解决方案;在对试卷生成算法的介绍中,本文提出“探索法”解决试卷抽题的方案。     

计算机无纸考试系统上机考试软件设计

非计算机专业计算机基础系列课程教学是我国高等院校的重要教学内容。上机操作和程序设计等客观考试方式是加强大学生能力培养的重要手段。本文在分析了各种无纸考试系统和题库系统的基础上，提出了无纸考试系统三段式设计新构想，并采用了驻留、仿真、直接磁盘写等关键技术，解决了单任务操作系统ＤＯＳ的不可重入问题。本文着重介绍三段式设计思想和第二阶段计算机无纸考试系统上机考试软件的设计。     

多功能显示系统中的矢量字符构成方法

介绍了航电多功能显示系统(MFDS)中字符的构造方法,具体阐述了一种用于MFDS的矢量字符构造方法。     

字符发生器的一种设计方案

提出了一种采用SOC单芯片设计字符发生器的方法;介绍了SOC芯片的特性;给出了字符发生器的设计框图;并讨论了设计过程中的若干问题。     

用于雷达波形的无损压缩编码

讨论了用算术编码实现波形数据的无损压缩。对波形数据进行无损压缩时 ,如果把每个可能的样本值看作一个符号 ,符号表会非常庞大 ,导致算法不可行。基于这种原因 ,本文用一个符号表示一定范围内波形数据 ,而不是单个波形数据 ,然后在此基础上设计了一种编码方案。先是无损线性预测 ,去除了波形数据之间的相关性。并假定产生的差值序列具有白功率谱 ,幅度服从高斯分布 ,第二步是算术编码。最后给出了对雷达回波数据进行压缩的实验结果。     

梯型螺母中径综合误差值分析

在机械传动中,梯形丝杠与大小螺母的配合是一种常见的结构,而梯形丝杠中的大、小螺母的加工又是一个关键问题,结合工程实际提出了梯型螺母在加工检验中存在的中径精度问题,并就此问题进行了详细讨论和理论分析,并且给出了解决问题的方法,对于同类零件的加工也具有指导意义.     

Multi-h CPM遥测信号的定时频率联合估计技术

针对Multi-h CPM（Multi-h Continue Phase Modulation,多指数连续相位调制）遥测接收机的符号定时和载波频率同步问题,在分析MLSD（Maximum-likelihood Sequence Detection,最大似然序列检测）度量值是符号定时偏差和频率偏差的凸函数的基础上,提出一种基于迟/早门和升/降频门的符号定时和频率同步联合估计算法,通过似然值比较,对符号定时偏差和频率偏差进行迭代估计;并对该算法进行仿真,得到不同参数下的同步性能,给出同步参数选择建议.仿真结果表明：将该算法应用到Multi-h CPM遥测系统中,可实现低信噪比信号的快捕和高精度同步.     

信息隐藏技术中二维条码的实现

介绍了二维条码符号表示及纠错码生成,给出二维条码用于信息隐藏技术的方法和途径,实现了用 PDF417码传送信息,使通信信息更安全。     

Carrier Tracking by Smoothing Filter Improves Symbol SNR

The potential benefit of using a smoothing filter to estimate a carrier phase over use of phase-locked loops (PLL) is determined. Numerical results are presented for the performance of three possible configurations of an all-digital coherent demodulation receiver. These are residual carrier PLL, sideband-aided residual carrier PLL, and finally sideband aided with Kalman smoother. The average symbol SNR after losses due to carrier phase estimation is computed for different total power SNRs, symbol rates, and symbol SNRs. It is found that smoothing is most beneficial for low symbol SNRs and low symbol rates. Smoothing gains up to 0.7 dB over sideband-aided residual carrier PLL, and the combined benefit of smoothing and sideband aiding relative to residual carrier loop is often in excess of 1 dB.     

遥测系统中喷泉码的低延时改进算法

针对喷泉码应用于遥测系统时存在较大系统延时的问题,在对其延时特性进行分析的基础上,提出了一种改进的编译码算法.当编码器接收到部分数据符号时,按照预先制定的度选取策略和符号选取策略,选择当前编码符号的度和生成该编码符号的数据符号进行编码.该算法以减小编码延时为目标,通过分析编码符号发送速率的稳定性和可容忍的最长信号闪断时间可确定合理的编码延时.仿真得到了不同丢符号率下的编码延时、系统延时和所需的编码冗余,结果表明,与传统方案相比,改进方案的编码延时减小了一半以上.通过理论分析和仿真验证,得出了改进算法可明显减小基于喷泉码的遥测系统延时的结论.