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

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

摘要:矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.

摘要:矩阵是工程领域中常用的一种数据结构，在深度学习领域，矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题，分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算，并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结，并且分析了矩阵形式化的主要几种方法；其次介绍并完善了基于Coq记录类型的矩阵形式化方法，其中包括提出新的矩阵等价定义、对之前的形式化工作进行了整理和完善，并证明了一组新的引理；在此基础上，进一步实现了分块矩阵运算的形式化，讨论了该类型归纳证明的难点和解决方法；最终实现了矩阵与分块矩阵形式化的不同类型的基础库.

摘要:复杂对象是现实世界复杂实体的抽象与描述,CIMS、CAD和OA等许多应用领域需要定义和操纵复杂对象,本文给出了复杂对象模型的定义,并论述了面向对象数据库系统WHYMX的复杂对象并发控制机制。