微信服务号

微信订阅号

2025-4-24- 19
Home > Archive>Volume 29, Issue 6, 2018 >1699-1715. DOI:10.13328/j.cnki.jos.005468
PDF HTML XML Export Cite reminder
Modeling and Verification for Robot Joint Bus Communication System
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61373034, 61572331, 61472468, 61602325); the National KeyTechnology Research and Development Program (2015BAF13B01); the International Cooperation Program on Science and Technology(2011DFG13000); the Project of Beijing Municipal Science & Technology Commission (LJ201607); the Project of Construction ofInnovative Teams and Teacher Career Development for Universities and Colleges Under Beijing Municipality (IDHT20150507); theScientific Research Base Development Program of the Beijing Municipal Commission of Education (TJSHG201510028010)

  • Article
    • | |
  • Metrics
    • |
  • Reference [30]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    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.

    Reference
    [1] Nilsson DK, Larson UE, Picasso F, Jonsson E. A first simulation of attacks in the automotive network communications protocol flexray. In:Proc. of the Int'l Workshop on Computational Intelligence in Security for Information Systems (Cisis 2008). Genova:DBLP, 2009. 84-91.[doi:10.1007/978-3-540-88181-0_11]
    [2] Wang DQ, Gao SY, Chen YQ, Wang Y, Liu Q. Intelligent control system based on CAN-bus for car doors and windows. In:Proc. of the Int'l Conf. on Anti-Counterfeiting, Security, and Identification in Communication. IEEE, 2009. 242-245.[doi:10.1109/ICASID.2009.5276906]
    [3] Sabelhaus AP, Bruce J, Caluwaerts K, Manovi P. System design and locomotion of SUPERball, an untethered tensegrity robot. In:Proc. of the IEEE Int'l Conf. on Robotics and Automation (ICRA). IEEE, 2015. 2867-2873.[doi:10.1109/ICRA.2015.7139590]
    [4] Kaneko K, Harada K, Kanehiro F, Miyamori G. Humanoid robot HRP-3. In:Proc. of the IEEE/RSJ Int'l Conf. on Intelligent Robots and Systems. IEEE, 2008. 2471-2478.[doi:10.1109/IROS.2008.4650604]
    [5] Kim JY, Park IW, Lee J, Kim MS, Cho BK, Oh JH. System design and dynamic walking of humanoid robot KHR-2. In:Proc. of the IEEE Int'l Conf. on Robotics and Automation. IEEE, 2005. 1431-1436.[doi:10.1109/ROBOT.2005.1570316]
    [6] Li XY, Huang M, Zhan J, Ni YL, Pang FY. CANoe-Based modeling and simulation for heavy lorry CAN bus network. In:Proc. of the AsiaSim 2012. Berlin, Heidelberg:Springer-Verlag, 2012. 107-114.[doi:https://doi.org/10.1007/978-3-642-34387-2_13]
    [7] Liu T, Wang SL, Zhan NJ. Safety verification of trajectory planning for multiple robots. Ruan Jian Xue Bao/Journal of Software, 2017,28(5):1118-1127(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5207.htm[doi:10.13328/j.cnki.jos. 005207]
    [8] Resten Y, Maler O, Marcus M, Pnueli A, Shahar E. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 2001,256(1-2):93-112.[doi:https://doi.org/10.1016/S0304-3975(00)00103-1]
    [9] Xiao D, Zhu YF, Liu SL, Wang DX, Luo YQ. Applied Mechanics & Materials. 2015,716-717:1382-1386.[doi:10.4028/www. scientific.net/AMM.716-717.1382]
    [10] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.[doi:10.1016/0304-3975(94) 90010-8]
    [11] Berendsen J, Gebremichael B, Vaandrager FW, Zhang MM. Formal specification and analysis of zeroconf using uppaalS. ACM Trans. on Embedded Computing Systems, 2011,10(3):1-32.[doi:10.1145/1952522.1952527]
    [12] Pan C, Guo J, Zhu LF. Modeling and verification of CAN bus with application layer using UPPAAL. Electronic Notes in Theoretical Computer Science, 2014,309:31-49.[doi:https://doi.org/10.1016/j.entcs.2014.12.004]
    [13] Gu JS, Silva CWD. Development and implementation of a real-time open-architecture control system for industrial robot systems. Engineering Applications of Artificial Intelligence, 2004,17(5):469-483.[doi:10.1016/j.engappai.2004.03.010]
    [14] Behrmann G, David A, Larsen KG. A tutorial on UPPAAL. In:Bernardo M, ed. Proc. of the Formal Methods for the Design of Real-Time Systems. Springer-Verlag, 2004. 200-236.[doi:10.1007/978-3-540-30080-9_7]
    [15] Dai SX, Hong M, Guo B, Yang QH, Huang W, Xu BP. Schedulability analysis model for multiprocessor real-time systems using UPPAAL. Ruan Jian Xue Bao/Journal of Software, 2015,26(2):279-296(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4781.htm[doi:10.13328/j.cnki.jos.004781]
    [16] Battiston A. Software in C++ for communication between CAN bus and ROS in a robot vehicle[Ph.D. Thesis]. Padua University, 2014.
    [17] Behrmann G, David A, Larsen KG. A tutorial on uppaal. In:Proc. of the Formal Methods for the Design of Real-Time Systems. Berlin, Heidelberg:Springer-Verlag, 2004. 200-236.
    [18] Dong YK. Research on scheduling algorithm based on CAN bus[Ph.D. Thesis]. Beijing:Tsinghua University, 2011(in Chinese).
    [19] Führer T, Müller B, Dieterle W, Hartwich F, Hugel R, Walther M, Gmbh RB. Time triggered communication on CAN. In:Proc. of the Time Triggered CAN (TTCAN). Bibliogr, 2001.
    [20] Zuberi KM, Shin KG. Non-Preemptive scheduling of messages on controller area network for real-time control applications. In:Proc. of the 1st IEEE Real-Time Technology and Applications Symp. (RTAS'95). Chicago:IEEE Computer Society, 1995. 240-249.
    [21] Davis RI, Burns A, Bril RJ, Lukkien JJ. Controller area network (CAN) schedulability analysis:Refuted, revisited and revised. Real-Time Systems, 2007,35(3):239-272.[doi:10.1007/s11241-007-9012-7]
    [22] Liu JF, Gui WH, Huang ZW, et al. Study of the application on a scheduling algorithm of CAN bus in locomotive brake. Journal of Chinese Computer Systems, 2009,30(1):183-187(in Chinese with English abstract).
    [23] Davis RI, Kollmann S, Pollex V, et al. Controller area network (CAN) schedulability analysis with FIFO queues. In:Proc. of the Euromicro Conf. on Real-Time Systems. IEEE Computer Society, 2011. 45-56.[doi:10.1109/ECRTS.2011.13]
    [24] Anwar K, Khan ZA. Dynamic priority based message scheduling on controller area network. In:Proc. of the Int'l Conf. on Electrical Engineering. IEEE, 2007. 1-6.[doi:10.1109/ICEE.2007.4287302]
    [25] Murtaza AF, Khan ZA. Starvation free controller area network using master node. In:Proc. of the Int'l Conf. on Electrical Engineering. IEEE, 2008. 1-6.[doi:10.1109/ICEE.2008.4553945]
    附中文参考文献:
    [7] 刘涛,王淑灵,詹乃军.多机器人路径规划的安全性验证.软件学报,2017,28(5):1118-1127. http://www.jos.org.cn/1000-9825/5207.htm[doi:10.13328/j.cnki.jos.005207]
    [15] 代声馨,洪玫,郭兵,杨秋辉,黄蔚,徐保平.多处理器实时系统可调度性分析的UPPAAL模型.软件学报,2015,26(2):279-296. http://www.jos.org.cn/1000-9825/4781.htm[doi:10.13328/j.cnki.jos.004781]
    [18] 董寅康.基于CAN总线的调度算法的研究[博士学位论文].北京:清华大学,2011.
    [22] 刘剑锋,桂卫华,黄志武,等.一种CAN总线调度算法在机车制动机上的应用研究.小型微型计算机系统,2009,30(1):183-187.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

孟瑶,李晓娟,关永,王瑞,张杰.机器人关节通信总线系统的建模与验证.软件学报,2018,29(6):1699-1715

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 01,2017
  • Revised:September 01,2017
  • Adopted:December 05,2017
  • Online: December 28,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038239Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063