Page 52 - 《软件学报》2025年第8期

张善强 等: 单球驱动平衡机器人运动学和动力学形式化验证 3475

[11] Fankhauser P, Gwerder C. Modeling and control of a ballbot [B.S. Thesis]. Swiss Federal Institue of Technology Zurich, 2010. https://
www.researchgate.net/publication/259602161_Modeling_and_Control_of_a_Ballbot
[12] You YN, Ha HM, Kim YK, Lee JM. Balancing and driving control of a ball robot using fuzzy control. In: Proc. of the 12th Int’l Conf. on
Ubiquitous Robots and Ambient Intelligence. Goyangi: IEEE, 2015. 492–494. [doi: 10.1109/URAI.2015.7358812]
[13] Luckcuck M, Farrell M, Dennis LA, Dixon C, Fisher M. Formal specification and verification of autonomous robotic systems: A Survey.
ACM Computing Surveys (CSUR), 2019, 52(5): 100. [doi: 10.1145/3342355]
[14] Farooq B, Hasan O, Iqbal S. Formal kinematic analysis of the two-link planar manipulator. In: Proc. of the 15th Int’l Conf. on Formal
Engineering Methods on Formal Methods and Software Engineering. Queenstown: Springer, 2013. 347–362.
[15] Affeldt R, Cohen C. Formal foundations of 3D geometry to model robot manipulators. In: Proc. of the 6th ACM SIGPLAN Conf. on
Certified Programs and Proofs. Paris: ACM, 2017. 30–42. [doi: 10.1145/3018610.3018629]
[16] Barras B, Boutin S, Cornes C. The Coq proof assistant reference manual: Version 6.1. Technical Report, Inria: National Institute for
Research in Computer Science and Control, 1997. https://www.researchgate.net/publication/43140549_The_Coq_Proof_Assistant_
Reference_Manual_Version_61
[17] Wu AX, Shi ZP, Li YD, Wu MH, Guan Y, Zhang J, Wei HX. Formal kinematic analysis of a general 6R manipulator using the screw
theory. Mathematical Problems in Engineering, 2015, 2015(1): 549797. [doi: 10.1155/2015/549797]
[18] Chen Q, Wang GH, Zhang QY, Shi ZP, Chen SY, Guan Y. Formal modeling and verification of planar parallel mechanism. Journal of
Chinese Computer Systems, 2020, 41(5): 925–931 (in Chinese with English abstract). [doi: 10.3969/j.issn.1000-1220.2020.05.005]
[19] Xie GJ, Yang HH, Shi ZP, Chen G. Formal verification of robot forward kinematics based on DH calibration. Ruan Jian Xue Bao/Journal
of Software, 2024, 35(9): 4160–4178 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/7131.htm [doi: 10.13328/j.cnki.
jos.007131]
[20] Abed S, Rashid A, Hasan O. Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving. Journal of
Aerospace Information Systems, 2020, 17(9): 481–495. [doi: 10.2514/1.I010730]
[21] Rashid A, Hasan O. Formal analysis of robotic cell injection systems using theorem proving. In: Proc. of the 7th Int’l Workshop on Cyber
Physical Systems. Design, Modeling, and Evaluation. Seoul: Springer, 2019. 127–141. [doi: 10.1007/978-3-030-17910-6_10]
[22] Zhang JZ. Formalization of generalized variational and Lagrangian mechanics and applications to robot dynamics [Ph.D. Thesis]. Beijing:
Capital Normal University, 2020 (in Chinese with English abstract).
[23] Zhang JZ, Wang GH, Shi ZP, Guan Y, Li YD. Formalization of functional variation in HOL Light. Journal of Logical and Algebraic
Methods in Programming, 2019, 106: 29–38. [doi: 10.1016/j.jlamp.2019.04.004]
[24] Guan Y, Zhang JZ, Wang GH, Li XM, Shi ZP, Li YD. Formalization of Euler-Lagrange equation set based on variational calculus in
HOL Light. Journal of Automated Reasoning, 2021, 65(1): 1–29. [doi: 10.1007/s10817-020-09549-w]
[25] Harrison J. HOL Light: A tutorial introduction. In: Proc. of the 1st Int’l Conf. on Formal Methods in Computer-aided Design. Palo Alto:
Springer, 1996. 265–269. [doi: 10.1007/BFb0031814]
[26] Paulson LC. ML for the Working Programmer. 2nd ed., New York: Cambridge University Press, 1996.
[27] Qasim U, Rashid A, Hasan O. Formalization of bond graph using higher-order-logic theorem proving. ISA Trans., 2022, 128: 453–469.
[doi: 10.1016/j.isatra.2021.11.042]
[28] Nagarajan U, Mampetta A, Kantor GA, Hollis RL. State transition, balancing, station keeping, and yaw control for a dynamically stable
single spherical wheel mobile robot. In: Proc. of the 2009 IEEE Int’l Conf. on Robotics and Automation. Kobe: IEEE, 2009. 998–1003.
[doi: 10.1109/ROBOT.2009.5152681]
[29] Murray RM, Li ZX, Sastry SS. A Mathematical Introduction to Robotic Manipulation. Boca Raton: CRC Press, 1994. 36–37.
[30] Satici AC, Ruggiero F, Lippiello V, Siciliano B. Intrinsic Euler-Lagrange dynamics and control analysis of the ballbot. In: Proc. of the
2016 American Control Conf. Boston: IEEE, 2016. 5685–5690. [doi: 10.1109/ACC.2016.7526560]

附中文参考文献:
[4] 刘福才, 刘林, 李倩, 秦利, 王文魁. 重力对空间机构运动行为影响研究综述. 载人航天, 2017, 23(6): 790–797. [doi: 10.16329/j.
cnki.zrht.2017.06.013]
[5] 李政权. 人工智能时代的法律责任理论审思——以智能机器人为切入点. 大连理工大学学报 (社会科学版), 2019, 40(5): 78–87.
[doi: 10.19525/j.issn1008-407x.2019.05.010]
[6] 刘永谋. “机器人伤人”安全风险究竟在哪儿. 科学大观园, 2024, (2): 62–63 [doi: 10.3969/j.issn.1003-1871.2024.02.025]
[18] 陈琦, 王国辉, 张倩颖, 施智平, 陈善言, 关永. 平面并联机构的形式化建模与验证. 小型微型计算机系统, 2020, 41(5): 925–931. [doi: