基于xMAS模型的SpaceWire信誉逻辑的形式化验证

空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议, 保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。     

Cooperation and profit allocation in two-echelon logistics joint distribution network optimization

Collaborative two-echelon logistics joint distribution network can be organized through a negotiation process via logistics service providers or participants existing in the logistics system, which can effectively reduce the crisscross transportation phenomenon and improve the efficiency of the urban freight transportation system. This study establishes a linear optimization model to minimize the total cost of two-echelon logistics joint distribution network. An improved ant colony optimization algorithm integrated with genetic algorithm is presented to serve customer clustering units and resolve the model formulation by assigning logistics facilities. A two-dimensional colony encoding method is adopted to generate the initial ant colonies. Improved ant colony optimization combines the merits of ant colony optimization algorithm and genetic algorithm with both global and local search capabilities. Finally, an improved Shapley value model based on cooperative game theory and a cooperative mechanism strategy are presented to obtain the optimal profit allocation scheme and sequential coalitions respectively in two-echelon logistics joint distribution network. An empirical study in Guiyang City, China, reveals that the improved ant colony optimization algorithm is superior to the other three methods in terms of the total cost. The improved Shapley value model and monotonic path selection strategy are applied to calculate the best sequential coalition selection strategy. The proposed cooperation and profit allocation approaches provide an effective paradigm for logistics companies to share benefit, achieve win–win situations through the horizontal cooperation, and improve the negotiation power for logistics network optimization.     

用ENDEAVOUR软件鉴定肥胖症致病基因GAD2

鉴别复杂疾病致病基因对于治疗和预防疾病作用非常重要,致病基因预测软件是鉴别致病基因的有效工具。位于染色体10p12的基因GAD2是尚有争议的肥胖基因,许多研究者用实验方法研究基因GAD2,却得出了不一致的结论。基于生物计算的致病基因预测软件能弥补实验的不足,已成为揭示疾病发病机理和预测致病基因的有效途径,本文采用ENDEAVOUR软件来验证基因GAD2是否为肥胖症致病基因,该软件运用多种生物数据,根据每一个候选基因与已知致病基因的相似程度以排序,结果在35个候选基因中,基因GAD2排在最前面,表明基因GAD2最可能是肥胖症致病基因。预测结果有利于重新解释基因GAD2的生物功能,促使肥胖症药物的研制及治疗水平的提高。     

逼近点云的三角形网格的边缘误差减小研究

基于SOFM神经网络构建的三角形网格模型可以实现测量点云压缩后的Delaunay三角逼近剖分,但该模型存在边缘误差。为减小三角形网格的边缘误差,改进了三角形网格模型的训练模式,提出了3步训练模式。第1步采用整个测量点云,对三角形网格模型中的所有神经元进行整体训练;第2步采用测量点云中的边界点集,对三角形网格模型中的网格边界神经元进行训练;第3步采用边界点集中的角点点集,对与边界角点匹配最佳的网格边界神经元进行训练。算例表明,应用该训练模式,可以有效减小三角形网格的边缘误差,三角形网格逼近散乱点云的逼近精度得到提高并覆盖散乱点云整体分布范围。     

一种专门用于金属丝抗拉强度自动检测仪的夹紧机构的设计

介绍了一种能够自动检测金属丝抗拉强度的检测仪,并着重说明了专用夹紧机构的设计。该机构能够很好地解决在试件检测过程中的夹紧问题,从而有效地提高了检测过程的可靠性和工作效率,使设备更加适于生产现场的连续批量检测任务。