本公开涉及机器人，具体涉及一种单球驱动平衡机器人的运动学和动力学形式化验证方法。
背景技术：
1、单球驱动平衡机器人运动学和动力学问题分别描述了机器人末端和各个关节位置的几何关系，以及关节位置和力矩之间的力学关系。运动学和动力学的正确性有助于提高机器人的运行效率，保证机器人的安全性。所以，如何保证运动学和动力学方程的正确性，成为需要解决的迫切问题。
技术实现思路
1、本公开实施例提供一种单球驱动平衡机器人的运动学和动力学形式化验证方法。
2、第一方面，本公开实施例中提供了一种单球驱动平衡机器人的运动学和动力学形式化验证方法，包括：
3、建立单球驱动平衡机器人相关的坐标系；所述坐标系包括所述单球驱动平衡机器人的惯性坐标系、位于单球驱动平衡机器人球轮的球轮坐标系和位于单球驱动平衡机器人机身的机身坐标系；
4、建立齐次变换矩阵的高阶逻辑模型；所述齐次变换矩阵在形式化验证过程中，用于描述单球驱动平衡机器人的相关位姿，所述相关位姿包括单球驱动平衡机器人的末端位姿、球轮坐标系相对于惯性坐标系的位姿、机身坐标系相对于球轮坐标系的位姿；
5、建立矩阵值函数的微分的高阶逻辑模型和空间速度的高阶逻辑模型；
6、建立向量值函数有微分的高阶逻辑模型、向量值函数的微分的高阶逻辑模型、所述相关位姿中的旋转矩阵和位置向量的高阶逻辑模型；
7、建立单球驱动平衡机器人的拉格朗日方程的高阶逻辑模型；
8、利用齐次变换矩阵的高阶逻辑模型、矩阵值函数的微分的高阶逻辑模型、空间速度的高阶逻辑模型、向量值函数有微分的高阶逻辑模型、向量值函数的微分的高阶逻辑模型、拉格朗日方程的高阶逻辑模型，形式化描述单球驱动平衡机器人运动学和动力学相关的逻辑命题，运动学相关的逻辑命题包括末端位姿、空间速度、末端速度的逻辑命题；动力学相关的逻辑命题包括拉格朗日动力学方程的逻辑命题；
9、利用高阶逻辑定理证明器证明验证上述逻辑命题是否成立。
10、第二方面，本发明实施例中提供了一种单球驱动平衡机器人的运动学和动力学形式化验证装置，包括：
11、第一建立模块，被配置为建立单球驱动平衡机器人相关的坐标系；所述坐标系包括所述单球驱动平衡机器人的惯性坐标系、位于单球驱动平衡机器人球轮的球轮坐标系和位于单球驱动平衡机器人机身的机身坐标系；
12、第二建立模块，被配置为建立齐次变换矩阵的高阶逻辑模型；所述齐次变换矩阵在形式化验证过程中，用于描述单球驱动平衡机器人的相关位姿，所述相关位姿包括单球驱动平衡机器人的末端位姿、球轮坐标系相对于惯性坐标系的位姿、机身坐标系相对于球轮坐标系的位姿；
13、第三建立模块，被配置为建立矩阵值函数的微分的高阶逻辑模型和空间速度的高阶逻辑模型；
14、第四建立模块，被配置为建立向量值函数有微分的高阶逻辑模型、向量值函数的微分的高阶逻辑模型、所述相关位姿中的旋转矩阵和位置向量的高阶逻辑模型；
15、第五建立模块，被配置为建立单球驱动平衡机器人的拉格朗日方程的高阶逻辑模型；
16、形式化模块，被配置为利用齐次变换矩阵的高阶逻辑模型、矩阵值函数的微分的高阶逻辑模型、空间速度的高阶逻辑模型、向量值函数有微分的高阶逻辑模型、向量值函数的微分的高阶逻辑模型、拉格朗日方程的高阶逻辑模型，形式化描述单球驱动平衡机器人运动学和动力学相关的逻辑命题，运动学相关的逻辑命题包括末端位姿、空间速度、末端速度的逻辑命题；动力学相关的逻辑命题包括拉格朗日动力学方程的逻辑命题；
17、验证模块，被配置为利用高阶逻辑定理证明器证明验证上述逻辑命题是否成立。
18、所述功能可以通过硬件实现，也可以通过硬件执行相应的软件实现。所述硬件或软件包括一个或多个与上述功能相对应的模块。
19、第三方面，本公开实施例提供了一种电子设备，包括存储器和处理器；其中，所述存储器用于存储一条或多条计算机指令，其中，所述一条或多条计算机指令被所述处理器执行以实现第一方面所述的方法。
20、第四方面，本公开实施例提供了一种计算机可读存储介质，用于存储企业账户的安全认证装置所用的计算机指令，其包含用于执行上述第一方面所述方法所涉及的计算机指令。
21、应当理解的是，以上的一般描述和后文的细节描述仅是示例性和解释性的，并不能限制本公开。
1.一种单球驱动平衡机器人的运动学和动力学形式化验证方法，其特征在于，包括：
2.根据权利要求1所述的方法，其特征在于，所述运动学相关的逻辑命题包括末端位姿、空间速度、末端速度的逻辑命题；所述末端位姿的逻辑命题中使用齐次变换矩阵的高阶逻辑模型形式化描述末端位姿的求解过程；所述空间速度的逻辑命题中，使用矩阵值函数的微分的高阶逻辑模型形式化描述求解空间速度的前提条件后，用空间速度的高阶逻辑模型形式化描述空间速度的求解过程；所述末端速度的逻辑命题中使用矩阵指函数的微分和向量值函数有微分的高阶逻辑模型形式化描述求解末端速度的前提条件后，用向量值函数的微分的高阶逻辑模型形式化描述末端速度的求解过程。
3.根据权利要求1或2所述的方法，其特征在于，所述动力学相关的逻辑命题包括拉格朗日动力学方程的逻辑命题；其中，用所述惯性坐标系的xoz面的拉格朗日方程的高阶逻辑模型形式化描述所述单球驱动平衡机器人在垂直面上的拉格朗日动力学方程，所述垂直面上的拉格朗日动力学方程用于表达由所述单球驱动平衡机器人在垂直面上动能和势能计算驱动力矩；用所述惯性坐标系的xoy面的拉格朗日方程的高阶逻辑模型形式化描述所述单球驱动平衡机器人在水平面上的拉格朗日动力学方程，所述单球驱动平衡机器人在水平面上的拉格朗日动力学方程用于表达由所述单球驱动平衡机器人在水平面上动能和势能计算驱动力矩。
4.根据权利要求3所述的方法，其特征在于，用所述惯性坐标系的xoz面的拉格朗日方程的高阶逻辑模型形式化描述所述单球驱动平衡机器人在垂直面上的拉格朗日动力学方程时，选择单球驱动平衡机器人的末端相对于惯性坐标系的旋转角和单球驱动平衡机器人的末端相对于球轮的旋转角作为广义坐标，并根据所述广义坐标确定拉格朗日量和广义力；将确定的拉格朗日量代入拉格朗日方程，得到单球驱动平衡机器人在垂直面上的拉格朗日动力学方程。
5.根据权利要求3或4所述的方法，其特征在于，用所述惯性坐标系的xoy面的拉格朗日方程的高阶逻辑模型形式化描述所述单球驱动平衡机器人在水平面上的拉格朗日动力学方程时，选择球轮的旋转角度和机身的旋转角度作为广义坐标，并根据所述广义坐标确定拉格朗日量和广义力；将确定的拉格朗日量代入拉格朗日方程，得到单球驱动平衡机器人在水平面上的拉格朗日动力学方程。
6.一种单球驱动平衡机器人的运动学和动力学形式化验证装置，其特征在于，包括：
7.一种电子设备，其特征在于，包括存储器和处理器；其中，
8.一种计算机可读存储介质，其上存储有计算机指令，其特征在于，该计算机指令被处理器执行时实现权利要求1-5任一项所述的方法。
9.一种计算机程序产品，其包括计算机指令，其中，该计算机指令被处理器执行时实现权利要求1-5任一项所述的方法。
