论文部分内容阅读
近些年来，伴随着人工智能领域的浪潮，机器人越来越多地出现在我们的日常生活中，与我们的生活紧密相关，例如足球机器人、无人车、无人机等。这些机器人虽然不是安全攸关系统，但是一旦出现问题，仍然会对人民的生命财产造成直接威胁。因此，如何保证这些自治机器人尤其是多个机器人在移动过程中的安全成了人们一直很关心的问题。形式化方法因其具有严格的数学基础而被广泛应用于软硬件系统的规约和验证中，本论文即是用混成通信顺序进程和混成霍尔逻辑来对多机器人的路径规划算法进行建模并验证。 混成通信顺序进程(Hybrid Communicating Sequential Process，HCSP)是一个针对混成系统的形式化建模语言，它在通信顺序进程(Communicating Sequential Process，CSP)的基础上引入了微分方程来对系统的连续行为进行建模，同时引入中断机制（条件中断、超时中断和通信中断）来描述连续动态行为和离散控制行为交错运行的情形。HCSP可以方便地对大型控制系统尤其是在有通信事件发生时的情形进行形式化建模。混成霍尔逻辑作为霍尔逻辑的混成扩充，是HCSP的逻辑推理系统。它的定理证明器HProver能够对HCSP模型进行定理证明。但是由于目前的HProver无法处理向量和矩阵数据类型，因此本论文首先对HProver进行扩展，然后用HCSP对多机器人的路径规划算法D-CAPT进行建模，并在HProver中进行形式化验证。结果证明了该算法在满足一定的初始条件下，机器人团队在整个运行过程中不会碰撞。最后进一步考虑了在有加速度存在的条件下该算法的验证。