机械化验证一个高效的迭代数据流求解算法

迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.

基于高频信号注入的同步电机无传感器控制

针对现有低速同步电机无传感器控制精度低、运算复杂的问题,提出了一种适用于静止和低速应用场合的高频电压信号注入的同步电机无传感器驱动控制方法(椭圆拟合技术)。首先,建立了永磁同步电动机(PMSM)的数学模型,分析了椭圆拟合技术判断永磁同步电机转子位置的原理;其次,通过对比线性最小二乘法问题的3种求解方法,显示了QR分解法的优势,并提出了椭圆拟合技术中QR分解原理;最后,在两种不同的控制平台下进行了实验验证。结果表明所提出的椭圆拟合技术不受信号处理延迟效应的影响,响应速度快;只需调整遗忘因子一个参数,设置简单,适用于工业领域的广泛应用。