单光栅非干涉图像法测量大位移及其地址码的修正

提出非干涉图像法测量物体大位移的方法，即利用两个正交的图像记录系统，在试件作大位移后，记录被平行多光束照射形成的光点所覆盖的试件图像，借助于记录光路系统几何参数，可建立联立方程组．解此方程组，就可得到被测物体上诸光点所表示的测点的位移大小和坐标值．文中还论述了试件图像上测点位置的确定和修正方法，推导了被测物体图像负片上测点的实际坐标的计算公式．实验结果证明，本文提出的测量理论是正确的．     

基于接口精化的广义无干扰性研究

在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中,信息流安全属性仅局限于二元安全级格模型的问题,在现有安全接口结构基础上提出广义安全接口结构,在广义安全接口结构上定义精化关系,并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性,首次将安全多执行的思想应用于构件化系统的信息流安全属性验证.使用Coq定理证明工具实现了接口自动机程序库以及对精化关系的判定过程,并用实例验证说明了无干扰属性定义的特点及判定方法的有效性.     

基于无干扰理论的虚拟机可信启动研究

云计算作为一种新型高价值计算系统,目前被广泛应用于各行业领域;等保2.0中也提出了对其应用主动免疫可信计算技术进行动态可信验证的要求.云计算模式下,虚拟机作为用户使用云服务的直接载体,其可信启动是虚拟机运行环境可信的基础.但由于虚拟机以进程的形式运行在物理节点上,其启动过程呈现出高动态性,且多虚拟机域间存在非预期干扰等特点;而现有的虚拟机可信启动方案存在虚拟机启动过程的动态防护性不足、缺乏多虚拟域间非预期干扰性排除等问题.针对上述问题,提出一种基于无干扰理论的虚拟机可信启动研究方案.首先,基于无干扰理论,提出了虚拟机进程的运行时可信定理;进一步地,给出了虚拟机可信启动的定义并证明了虚拟机可信启动判定定理.其次,依据虚拟机可信启动判定定理,基于系统调用设计监测控制逻辑,对虚拟机启动过程进行主动动态度量与主动控制.实验结果表明所提方案能够有效排除复杂云环境下多虚拟机间非预期干扰,保证虚拟机启动过程的动态可信性,且性能开销较小.     

蜂窝芯零件五坐标加工无干涉建模

从曲面整体连续性、可加工性的角度,提出了一种组合曲面整体G^1连续模型的建立方法,并推导出曲面过渡区域五坐标加工时无局部过切干涉的条件．为了保证方向舵表面铺层和蜂窝芯之间的胶结强度,避免加工过程中的局部过切干涉,分析了复杂过渡曲面区域的设计方法,获得了既能保证整体连续性又能保证可加工性的高品质曲面模型．     

基于遗传算法的多主轴头加工空行程轨迹规划

针对多主轴头五轴机床加工时需手动规划空行程的问题,提出一种空行程轨迹自动规划方法。在机床运动学建模的基础上,针对刀位点轨迹和刀轴矢量,分别提出基于最短路径的刀位点轨迹规划和无碰撞刀轴矢量规划,将空行程规划问题转化为参数优化问题。为了简化碰撞检测,提出两级相交检测算法。通过加权系数法建立空行程规划的目标函数,并采用遗传算法求解,规划出一条无碰撞、运动时间最短、旋转轴角度变化量最小、末端轨迹最短的具有柔性的理想轨迹。在Vericut建立的仿真平台上,验证了该方法的可行性和有效性。所提方法具有拓展性,通过多次分解轨迹求取棱交点能够实现复杂工件的空行程规划。     

最优加权矩阵的选取

在最优控制系统设计中,由于二次型评价函数和闭环系统的关系不明,往往采用试探法选取加权矩阵Q、R。这样不仅难以选定最优参数,也给控制系统的现场调试带来了很大的困难。本文阐述了一种选取加权矩阵的新方法——零点追加法。     

光开关的技术现状和展望

光开关是光通信的关键部件,是近年来通信领域的研究热点.文章从光开关的实现方式等方面介绍了光开关的研究与生产现状,重点介绍了MEMS光开关的研究与应用,对光开关发展趋势作了分析.     

一种面向非干扰的线程程序逻辑

目前,针对线程信息流的验证研究主要着重于时间信道.然而,由于线程程序中线程控制原语存在函数副作用,对此类原语的不恰当调用亦可引起非法信息流,有意或无意地破坏程序的非干扰属性.因此,提出以验证线程程序信息流为目的依赖逻辑,其可表达线程程序的数据流、控制流以及线程控制函数的副作用,推理程序变量和线程标识符之间的依赖关系,进而判定是否存在高机密性变量对低机密性变量的干扰.     

Proving the correctness of client/server software

Remote procedure calls (RPCs) lie at the heart of any client/server software. Thus, formal specification and verification of RPC mechanisms is a prerequisite for the verification of any such software. In this paper, we present a mathematical specification of an RPC mechanism and we outline how to prove the correctness of an implementation—say written in C—of this mechanism at the code level. We define a formal model of user processes running concurrently under a simple operating system, which provides inter-process communication and portmapper system calls. A simple theory of non-interference permits us to use conventional sequential program analysis between system calls (within the concurrent model). An RPC mechanism is specified and the correctness proof for server implementations, using this mechanism, is outlined. To the best of our knowledge this is the first treatment of the correctness of an entire RPC mechanism at the code level.