实数二项式系数在HOL4中的形式化

定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。     

电容劣化对DC-DC电源寿命影响仿真系统

在DC-DC电源中,滤波网络中铝电解电容的劣化是影响电源寿命的主要因素,因此可以通过监测电容的劣化来评估DC-DC的健康状况。基于前期对电容的主要劣化模式及其对DC-DC影响的研究工作建立了电容劣化对DC-DC寿命影响仿真系统。该系统以LabView为主设计完成,通过劣化注入的方式模拟电容劣化。系统测试结果：电容劣化引起DC-DC输出纹波电压变大,DC-DC寿命缩短,这与理论分析一致。该系统可以仿真电容劣化的过程并可研究电容劣化对DC-DC寿命的影响。     

星载SpaceWire路由器的研究与设计

为满足航天器有效载荷间高速数据多路传输的未来发展需求,该文研究提出了基于SpaceWire的星载数据路由的设计方案。在SpaceWire总线标准网络层分析的基础上,结合虫孔路由原理构建路由器内部结构,提出了采用无阻断交差开关的SpaceWire路由器设计方案。在Simulink环境下建立了路由器仿真模型,并通过BWR解决了虫孔路由阻塞机制带来的刹车问题,使路由器的满负荷通信下的平均丢包率减少了70％。     

数字音乐合成器的研究与设计

音色与灵活性是音乐合成器的两个重要指标;为结合两者特点,根据数字FM合成法和采样回放合成法,以吉他为例对关键周期波形的时域包络处理和频域调制实现了一种新的数字音乐合成方法。实验表明：合成效果能较好表现音色,并有一定的设计灵活性。通过MATLAB在计算机上实现设计,为便携式、小型化数字音乐合成设备的设计提供了参考。     

基于经验公式的制动气室动态特性分析

制动气室作为汽车防抱死制动系统的执行元件,其动态特性影响整个制动系统的性能.为此,在分析制动气室原理的基础上,通过对试验测试数据的FDD启发式搜索验证了经验公式,并用最小二乘法尝试拟合了待定参数的函数关系;在SIMULINK下的仿真结果表明,在引入制动气室动态特性参数分析后,能有效提高制动过程的有效性和可靠性.     

机器人控制系统关键模块的形式化验证

随着机器人应用在越来越多的领域,人们对其安全性的要求越来越高,作为机器人的核心,控制系统设计的可靠性对整个系统的安全至关重要;针对一种模块化设计的机器人控制系统架构,利用xMAS(eXecutable MicroArchitecture Specification,可执行微架构描述)模型在定理证明器ACL2中对其功能正确性进行验证,首先对Xmas在ACL2中的形式化理论做了阐述,然后对该机器人控制系统中的加速度传感器数据采集模块建立xMAS模型,提取关键属性并进行验证;将xMAS模型和定理证明器ACL2相结合,可以很好地解决机器人控制系统的验证问题,为机器人控制系统的形式化验证提供一个有效的方法参考。     

基于参数限定的CS-RBF曲面重建算法*

针对非密度均匀的点云,提出了一种高效保持特征的曲面重建算法。首先利用八叉树进行点云空间分割,然后对每个点在小邻域内求出局部逼近曲面,建立隐式曲面方程。通过参数限定点的邻域范围,使整个算法既保证了重建效果,又不致于很大程度上增加重建时间,达到了速度和效果在一个范围内的平衡。实验结果证明,本算法重建效果良好,适用于各种散乱点云的重建。     

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.     

实时嵌入式双操作系统架构研究综述

随着全球工业4.0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系统和通用操作系统.本文归纳总结国内外嵌入式双操作系统的研究现状,对各种实现技术进行深入探讨和分析,列举嵌入式双操作系统典型应用和主要应用领域,最后对该类技术的研究趋势进行总结.