主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
孟瑶,李晓娟,关永,王瑞,张杰.机器人关节通信总线系统的建模与验证.软件学报,2018,29(6):1699-1715
机器人关节通信总线系统的建模与验证
Modeling and Verification for Robot Joint Bus Communication System
投稿时间:2017-07-01  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005468
中文关键词:  形式化验证  实时性  时间自动机  CAN  动态优先级
英文关键词:formal verification  real-time  timed automata  CAN  dynamic priority
基金项目:国家自然科学基金(61373034,61572331,61472468,61602325);国家科技支撑计划(2015BAF13B01);国际科技合作计划(2011DFG13000);北京市科委项目(LJ201607);北京市教委科研基地建设项目(TJSHG201510028010);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)
作者单位E-mail
孟瑶 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
 
李晓娟 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
lixj@cnu.edu.cn 
关永 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
 
王瑞 首都师范大学 信息工程学院, 北京 100048
轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048 
 
张杰 北京化工大学 信息科学与技术学院, 北京 100029  
摘要点击次数: 828
全文下载次数: 594
中文摘要:
      高速串行现场总线(controller area network,简称CAN)被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点,因此,如何根据总线协议规范和应用需求精化设计模型,保证系统设计的正确性和实时性要求,避免设计阶段的漏洞十分必要.针对传统方法的局限性,提出使用形式化方法对基于CAN现场总线型控制系统进行建模分析.首先,对系统进行模型抽象和形式表达;其次进行形式建模和自动验证,在UPPAAL中实现主控制器、关节控制器、收发器、仲裁器和CAN总线的时间自动机模型;最后对机器人通信系统进行正确性验证和实时性分析.实时性分析发现:随着总线上关节节点数的增多,低优先级节点的最坏仲裁时延的增长速率加大.针对这个问题,在形式模型中加入了改进的动态优先级策略.实验结果表明:部署动态优先级策略后不仅减小了低优先级节点的仲裁时延,而且还可以加大CAN总线的节点负载量,为系统设计提供有效的指导和参考.
英文摘要:
      Controller area network (CAN) is a high-speed serial fieldbus, widely deployed in the robot communication system. Due to the concurrency of service-oriented robot tasks and tightness requirement for real-time, it is necessary to explore how to refine the design model according to the bus protocol specifications and application system, in order to ensure the correctness and real-time requirements of the system and avoid bugs in design process. However the traditional methods are limited. This paper proposes a formal method to verify and analyze the correctness of CAN based fieldbus real-time control system. The model abstraction, formal modeling and automatic verification are presented for the system including the time automata model of master, joint controller, transceiver, arbitration and CAN bus. The formal models show that the worst arbitration delay of the low priority node increases rabidly with the increasing number of joints on the CAN bus. Furthermore, an improved dynamic priority strategy is designed and added into the formal models in order to improve the worst arbitration delay problem. The experimental results show that the deployment of the dynamic priority strategy not only reduces the arbitration delay of the low priority nodes, but also increases the capacity of nodes on CAN bus. The result provides guidance and effective reference for the system design.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利