机器人关节通信总线系统的建模与验证

来源：软件学报杂志2018年第6期北京时间：

作者：孟瑶,李晓娟,关永,王瑞,张杰

单位：孟瑶，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004811,李晓娟，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004802,关永，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004803,王瑞，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004804,张杰，北京化工大学 信息科学与技术学院, 北京 10002905

摘要：高速串行现场总线（controller area network，简称CAN）被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点，因此，如何根据总线协议规范和应用需求精化设计模型，保证系统设计的正确性和实时性要求，避免设计阶段的漏洞十分必要.针对传统方法的局限性，提出使用形式化方法对基于CAN现场总线型控制系统进行建模分析.首先，对系统进行模型抽象和形式表达；其次进行形式建模和自动验证，在UPPAAL中实现主控制器、关节控制器、收发器、仲裁器和CAN总线的时间自动机模型；最后对机器人通信系统进行正确性验证和实时性分析.实时性分析发现：随着总线上关节节点数的增多，低优先级节点的最坏仲裁时延的增长速率加大.针对这个问题，在形式模型中加入了改进的动态优先级策略.实验结果表明：部署动态优先级策略后不仅减小了低优先级节点的仲裁时延，而且还可以加大CAN总线的节点负载量，为系统设计提供有效的指导和参考.

关键词：形式化验证;实时性;时间自动机;CAN;动态优先级

基金资助：国家自然科学基金（61373034，61572331，61472468，61602325）；国家科技支撑计划（2015BAF13B01）；国际科技合作计划（2011DFG13000）；北京市科委项目（LJ201607）；北京市教委科研基地建设项目（TJSHG201510028010）；北京市属高等学校创新团队建设与教师职业发展计划（IDHT20150507）