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

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

分段线性电路切换系统的复杂行为及非光滑分岔机理

分析了分段线性电路系统在周期切换下的复杂动力学行为及其产生的机理. 基于平衡点分析, 给出了两子系统Fold分岔和Hopf分岔条件. 考虑了在不同稳定态时两子系统周期切换的分岔特性, 产生了不同的周期振荡, 并揭示了其产生的机理. 在不同的周期振荡中, 切换点的数量随参数变化产生倍化, 导致切换系统由倍周期分岔进入混沌. 关键词： 分段线性电路 切换系统 非光滑分岔     

CCD固体成像器件性能测试方法的研究

CCD图像传感器是目前科学成像领域主流的固体成像器件。一般而言, 当成像系统中使用CCD器件时, 首先需要测量它的一些性能指标, 这是判断该CCD器件是否满足整个系统性能要求的重要依据。对CCD成像器件性能的测试方法进行了探讨, 涉及的参数包括增益、噪声、电荷转移效率、线性和满阱电荷等。研究重点是如何应用扩展像素边界反应方法及同位素X射线方法检测CCD的电荷转移效率, 以及利用X射线方法测量器件的增益。最后以理论研究为基础, 发展并提出了一套切实可行的CCD器件检测方法, 同时基于E2V公司4K×4K芯片CCD203_82进行了性能测试实验, 实验结果也验证了本文提出的测试方法的可行性和可靠性。     

机器人控制系统串口模块的形式化验证

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