A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating programinvariants/inductive assertions.Given a program,inductive assertions,hypothesized as parameterizedformulas in a theory,are associated with program locations.Parameters in inductive assertions arediscovered by generating constraints on parameters by ensuring that an inductive assertion is indeedpreserved by all execution paths leading to the associated location of the program.The method can beused to discover loop invariants-properties of variables that remain invariant at the entry of a loop.Theparameterized formula can be successively refined by considering execution paths one by one;heuristicscan be developed for determining the order in which the paths are considered.Initialization of programvariables as well as the precondition and postcondition,if available,can also be used to further refinethe hypothesized invariant.The method does not depend on the availability of the precondition andpostcondition of a program.Constraints on parameters generated in this way are solved for possiblevalues of parameters.If no solution is possible,this means that an invariant of the hypothesizedform is not likely to exist for the loop under the assumptions/approximations made to generate theassociated verification condition.Otherwise,if the parametric constraints are solvable,then undercertain conditions on methods for generating these constraints,the strongest possible invariant of thehypothesized form can be generated from most general solutions of the parametric constraints.Theapproach is illustrated using the logical languages of conjunction of polynomial equations as well asPresburger arithmetic for expressing assertions.     

基于特征不变量的红外图像识别研究

给出了一种提取特征点的新方法和合理的特征不变量。该方法根据三角不等式原理利用第三边与另外两边之和的比值大小来确定角点,以特征点和它相邻的两个特征点所形成的两条直线的夹角正切值以及三角形第三边与另两边和的比值作为特征不变量。这种特征提取的方法简单,并且由于扩大了模板取值范围,使识别效果受特征点漏检的影响较小。实验表明,该方法不仅简便,而且效果良好。     

模式识别中的透射变换与仿射变换

仿射变换和透射变换是两种基本的图像变换。本文详细研究了仿射变换和透射变换的性质,并推导出它们之间的关系。研究表明,在特殊情况下,非线性的透射变换退变为线性的仿射变换;在多数情况下,透射变换可以用仿射变换很好地近似,这为透射变换的目标识别指出了一条新的途径。一组新的由低阶中心矩构成的仿射不变量验证了本文推导的正确性     

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems

Hybrid systems are dynamical systems with interacting discrete computation and continuous physical processes, which have become more common, more indispensable, and more complicated in our modern life. Particularly, many of them are safety-critical, and therefore are required to meet a critical safety standard. Invariant generation plays a central role in the verification and synthesis of hybrid systems. In the previous work, the fourth author and his coauthors gave a necessary and sufficient condition for a semi-algebraic set being an invariant of a polynomial autonomous dynamical system, which gave a confirmative answer to the open problem. In addition, based on which a complete algorithm for generating all semi-algebraic invariants of a given polynomial autonomous hybrid system with the given shape was proposed. This paper considers how to extend their work to non-autonomous dynamical and hybrid systems. Non-autonomous dynamical and hybrid systems are with inputs, which are very common in practice; in contrast, autonomous ones are without inputs. Furthermore, the authors present a sound and complete algorithm to verify semi-algebraic invariants for non-autonomous polynomial hybrid systems. Based on which, the authors propose a sound and complete algorithm to generate all invariants with a pre-defined template.     

一种脉冲多普勒雷达解速度模糊新方法

速度模糊是脉冲多普勒雷达中的一个重要问题。在没有别的信息源情况下,需要用雷达测得的距离信息来解速度模糊,因为距离回路输出与速度回路输出代表同一个目标的距离和径向速度,它们之间存在确定关系。推导最小二乘法解速度模糊的方法,提出一种新的不变量嵌入法解速度模糊的方法。通过理论分析和仿真证明不变量嵌入法可以有效地解速度模糊,并且实质上就是最小二乘法,其在提高距离精度上等效于测距、测速回路构成的复合控制系统。     

On the Parsimony of Some Model-Selection Criteria in Econometric Modeling

ＯｎｔｈｅＰａｒｓｉｍｏｎｙｏｆＳｏｍｅＭｏｄｅｌ－ＳｅｌｅｃｔｉｏｎＣｒｉｔｅｒｉａｉｎＥｃｏｎｏｍｅｔｒｉｃＭｏｄｅｌｉｎｇＺＨＡＮＧＷｅｉ；ＬＩＵＢａｏ（ＩｎｓｔｉｔｕｔｅｏｆＳｙｓｔｅｍＥｎｇｉｎｅｅｒｉｎｇ（ＩＳＥ），ＴｉａｎｊｉｎＵｎｉｖ...     

结构声辐射的虚边界元最小二乘法及仿真研究

提出用虚边界元最小二乘法研究结构体声辐射,推导了该方法计算振动结构辐射声场的计算公式,与常规边界元法相比,虚边界元最小二乘法避免了奇异积分的数值处理,且系数矩阵是对称的,通过仿真计算与解析解验证。结果表明,本文方法思想简单,程序处理容易,能够有效克服特征频率处解的非唯一问题,在边界附近解的精度较高等优点,便于工程应用。     

一类线性切换系统的能控性和能观测性的充要条件

循环不变子空间是常用于控制科学和信号处理理论的重要数学工具之一。用循环不变子空间的性质研究了切换系统的能控性和能观测性。先给出了切换系统能控性、能达性和能观测性的概念,并讨论了循环不变子空间的性质。然后用循环不变子空间的性质研究了周期线性切换系统的能控制性、能达性及能观测性,得到线性周期切换系统完全能控和完全能观测的充分必要条件。最后给出一般线性切换系统完全能控和完全能观测的充分条件和必要条件。     

一种新的多尺度仿射几何不变量提取方法

提出了一种新的多尺度仿射几何不变量提取方法。该方法以自定义的多尺度自卷积变换为起点,结合灰度归一化处理,构建出目标图像的一系列仿射协变形式,进而通过设计一组非线性函数计算每个协变形式的一组扩展质心,由此得到新的多尺度仿射几何不变量。将所得不变量与经典的扩展质心特征、多尺度自卷积相比,由于其仅需一次分割便可构造出任意数量的区域面积比仿射不变特征,且从单个仿射协变形式中即可提取多个不变特征,从而有效减小了特征误差,提高了特征的获取效率。利用典型的“Fish”测试数据库,从计算复杂度、抗噪性、抗遮挡性和图像扩展性等方面验证了所提方法的有效性。     

AHP中判断矩阵的区间权重及其一致性检验

AHP中由判断矩阵导出排序权重时,传统的方法只能得到"点"权重向量。为使结果更具柔性,考虑求解判断矩阵的区间权重向量。本文通过建立线性规划模型实现了这一点。与此同时,模型的最优值反映了判断矩阵的不一致性,故可借此进行一致性检验。通过模拟计算,对该检验方法和传统的通过计算CR值的方法间的相关性进行了统计分析。结果表明,二者具有显著的相关性。最后给出算例分析。     

用闭环增益成形算法的精馏塔鲁棒控制

给出了MIMO系统的闭环增益成形算法,将之应用于精馏塔的控制中,取得了良好的控制效果和鲁棒稳定性。文献［6］给出的回路成形控制器与本文的一阶闭环增益成形控制效果相同,文献［6］评价该法的不足之处是闭环系统的鲁棒性能稍差,该缺点可用本文的二阶或三阶闭环增益成形控制器加以克服。该算法的优点是设计过程简单,物理意义明显。     

基于状态信息的条件剩余寿命建模研究

根据监测到的设备状态信息预测其条件剩余寿命一直是基于状态维修中的关键问题。利用滤波理论,建立了基于状态信息的剩余寿命预测通用模型,并推导出采用极大似然估计法下参数估计的通式,使得在已知寿命服从其他任何分布形式时直接代入通式便可快速地得出其模型,从而预测其剩余寿命,省去了复杂繁琐的迭代过程。通过案例发现模型能够根据状态信息很好地预测其剩余寿命,并在不断更新状态信息的条件下越来越精确地预测其剩余寿命。     

矩阵变换器网侧相位无误差跟踪方法仿真研究

双级矩阵变换器(TSMC)因为换流相对简单,便于控制而成为当今研究的热点。在矩阵变换器整流级的控制中,电网相位的获取十分关键,在电网平衡时传统矩阵变换器是基于过零点检测进行相位获取。但是输入电压会出现波动、谐波、不平衡等干扰。这种非理想条件下,怎样实现电网相位的无误差跟踪便成为解决问题的关键。提出将改进的锁相环技术应用于输入三相电网电压的相位跟踪中,这是一种软件的锁相环技术,将改进的锁相环技术结合对称分量法应用于三相锁相环系统中,可以排除网侧输入电压的干扰,实现相位的无差跟踪。最后通过在MATLAB中搭建仿真模型,仿真结果证明这一方法可以很好的解决网侧输入不理想的问题。     

基于降阶观测器的双互质分解

基于降阶（非最小阶）观测器的设计,明确给出了一种新的线性时不变系统双互质分解的状态空间表示,并相应得到了真镇定控制器参数化结果的状态空间解释．与以往的结果相比,这种双互质分解更具一般性,更适用于稳定因式法.     

Causal association rule mining methods based on fuzzy state description

1.INTRODUCTIONIn the research of intricate systemcontrol andcompli-cated affair reasoning,the problemof mechanismandcomputational model of reasoning has become a veryi mportant issue in the academic world.Thus the re-search of indeterminacyinductive automatic reasoningmechanismis more i mportant.In the development of current logic science,ani mportant trendthat the research of logic thought andmethod merged into logic language has taken place.Thus the intelligence reasoning procedure is r…     

THE SYMMETRY GROUPS OF NONLINEARITY CRITERIA

It is already known that there are several nonlinearity criteria such as algebraic degree, nonlinearity,distance to linear structures, correlation immune, propagationcriterion, differential uniformity,which are used to check whether a cryptographic functionis weak or not. In this paper we will discuss these criteria from a valuation point of view,and consider the largest transformation group which leave a criterion invariant, which isnamed its symmetry group. It can serve as a way of comparing the stability of nonlinearitycriteria under the action of invertible transformations.     

基于横切关注点恢复的软件逆向工程研究

为解决软件遗产系统中横切特性的理解和进化问题,提出了面向侧面(aspect-oriented)的逆向工程框架模型,并以此为基础给出了一种用例驱动的形式化概念分析方法,对需求分析模型层面上的系统横切特性进行逆向恢复。通过对目标系统执行信息进行概念格分析,该方法能够识别和抽取横切用例模型的系统方法调用集合,并利用统一建模语言中用例图的版型(stereotype)机制对它们进行模型重构和呈现。与仅为了代码重构而进行的侧面挖掘(aspect mining)技术相比,该方法更适合在较高的系统抽象层面上进行程序理解,作为一种采用增量式结果产生策略的半自动化方法,它的实施流程也具有更好的可控性和对逆向工程需求变化的适应性。     

A Routing Algorithm for Distributed Optimal Double Loop Computer Networks

ＡＲｏｕｔｉｎｇＡｌｇｏｒｉｔｈｍｆｏｒＤｉｓｔｒｉｂｕｔｅｄＯｐｔｉｍａｌＤｏｕｂｌｅＬｏｏｐＣｏｍｐｕｔｅｒＮｅｔｗｏｒｋｓＬｉＬａｙｕａｎ（ＤｅｐａｒｔｍｅｎｔｏｆＥｌｅｃｔｒｉｃａｌＥｎｇｉｎｅｅｒｉｎｇａｎｄＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ．...     

基于预知信息的占线Nomadic TSP问题

自然灾害的频繁发生使得应急减灾倍受关注, 尤其有效的应急救援车辆调度对应急减灾非常重要. 针对受灾点被提前获知但是不能立即接受救援服务的情形, 通过将受灾点(需求)的揭露时间和释放时间引入Nomadic TSP模型中构建了预知信息的占线Nomadic TSP问题, 并分别给出了问题的下界, 直线网络结构下的ENO-dd算法, 和一般网络结构下的GTR-dd算法, 并对算法进行了竞争性能分析. 结果表明两个算法随着预知信息的增多会有明显改进. 更为一般的预知信息结构以及最优的算法设计是下一步研究的方向.