基于DH标定的机器人正向运动学形式化验证

DH坐标系在机器人运动学分析中发挥着重要的作用。在基于DH坐标系构建的机器人控制系统中,机器人结构的复杂性使得构建安全的控制系统成为一个难题,仅仅依靠人工方法可能导致系统漏洞和安全风险,从而危及机器人的安全。形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证。基于此,本文设计了基于DH标定的机器人正向运动学的形式化验证框架。在Coq中构建了机器人运动理论的形式化证明,并验证控制算法的正确性以确保机器人的运动安全。首先,对DH坐标系进行形式化建模,构建相邻坐标系间转换矩阵的形式化定义,并验证了该转换矩阵与复合螺旋运动的等价性;其次,构建了机械臂正向运动学的形式化定义,并对机械臂运动的可分解性进行形式化验证;再次,本文对工业机器人中常见连杆结构及机器人进行形式化建模,并完成了正向运动学的形式化验证;最后,本文实现了Coq到OCaml的代码抽取,并对抽取的代码进行分析与验证。     

多旋翼飞控推进子系统的Coq形式化验证

飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.     

基于柯西码的HDFS存储优化策略

随着大数据时代的到来,数据存储正接受着严峻的考验。为了改进传统Hadoop分布式文件系统HDFS存在的冗余度高、负载均衡能力不足等问题,提出了一种基于柯西码的动态分散式存储优化策略CDDS。对于系统中的数据块,在保证数据可用性的基础上,依据其热度的不同生成相应的存储方案。对于系统中的冷数据与热数据,分别采用基于柯西码的纠删码技术进行单副本与多副本存储,既保证了数据的可靠性又保证了系统的I/O能力。经测试,运用该策略存储数据所需要的存储空间减小为原来的75%,系统的可靠性与负载均衡能力也得到了增强。     

基于纠删码技术的云存储数据块部署方案

针对云存储系统中因忽视集群中存储节点之间的差异而引起的存储代价过高、可靠性较低、节点负载能力不足等问题,提出了段排序交换算法（FSSA）.首先对数据块部署问题进行数学建模;然后根据各个节点的负载情况进行分段,并在各个分段中依据数据可靠性的需求对节点进行初步选择;最后根据数学模型中对目标函数的分析在分段选择的结果中选取适当的节点进行数据部署.仿真结果表明,采用FSSA算法可以在保证数据存储可靠性的基础之上,降低数据存储代价、增强系统负载均衡能力.