Abstract
The Controller Area Network (CAN) is a message based communication service working over high-speed serial bus systems, and mostly used in the automotive industries and real-time communication systems. The CAN bus connects several independent CAN modules and allows them to communicate and work together asynchronously and/or synchronously. All nodes can simultaneously transmit data to the CAN bus, and the collision of multiple messages on the bus is resolved by a bitwise arbitration technique that operates by assigning a node with a low-priority message to switch to a “listening” mode while a node with a high-priority message remains in a “transmitting” mode. This arbitration mechanism results in the starvation problem that lower-priority messages continuously lose arbitration to higher-priority ones. This starvation is seen as a critical section problem with priority scheduling, where a synchronization technique is required at the entry and exit of the bus. The techniques of non-starvation critical section with general semaphore and barrier synchronization are applied to enable the CAN bus to proceed without starvation. In this paper, we present a formal model of a starvation-free bitwise CAN arbitration protocol applying barrier synchronization and starvation-free mutual exclusion. Based on SPIN Promela, we provide that the proposed CAN starvation-free CAN bus model works correctly.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Albert, A., Bosch, R.: Comparison of event-triggered and time-triggered concepts with regard to distributed control systems. Proc. Embed. World, 235–252 (2004)
CAN specification version 2.0. Robert Bosch GmbH, Stuttgart, Germany (1991)
Gil, J.A., et al.: A CAN architecture for an intelligent mobile robot. In: Proceedings of SICICA-97, pp. 65–70 (1997)
Fuhrer, T., et al.: Time-triggered Communication on CAN (Time-triggered CANTTCAN). In: Proceedings of ICC 2000, The Netherlands, Amsterdam (2000)
Hartwich F., et al.: Timing in the TTCAN network. In: Proceedings of 8th International CAN Conference, Las Vegas (2002)
Homepage of the organization CAN in Automation (CiA) (2004). http://www.can-cia.de
Rett, J.: Using the CANbus toolset software and the SELECONTROL MAS automation system, Control System Center, University of Sanderland (2001)
Magnenat S., et al.: ASEBA, an event-based middleware for distributed robot control. In: International Conference on Intelligent Robots and Systems (2007)
Davis, R.I., et al.: Controller Area Network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Syst. 35, 239–272 (2007)
Kimm, H., Kang, J.: Implementation of networked robot control system over controller area network. In: Proceedings of the Ninth IEEE International Conference on Ubiquitous Robots and Ambient Intelligence, Daejeon, Korea, 26–29 November 2012 (2012)
Pan, C., et al.: Modeling and verification of CAN bus with application Layer using UPPAL. Electron. Notes Theor. Comput. Sci. 309, 31–49 (2014)
Murtaza, A., Khan, Z.: Starvation free controller area network using master node. In: Proceedings of IEEE 2nd International Conference on Electrical Engineering, Lahore, Pakistan, 25–26 March 2008 (2008)
MSC8122: Avoiding Arbitration Deadlock During Instruction Fetch, FreeScale Semiconductor, INC. (2008)
Lee, K, et al.: Starvation Prevention Scheme for a Fixed Priority Pci\(-\)Express Arbiter with Grant Counters Using Arbitration Pools. US Patent Application Publication, 14 January 2009
Lin, C.-M.: Analysis and modeling of a priority inversion scheme for starvation free controller area networks. IEICE Trans. Inf. Syst. 93–D(6), 1504–1511 (2010)
Zago, G., de Freitas, E.: A quantitative performance study on CAN and CAN FD vehicular networks. IEEE Trans. Ind. Electron. 65(5), 4413–4422 (2018)
Park, P., et al.: Performance evaluation of a method to improve fairness in in-vehicle non-destructive arbitration using ID rotation. KSII Trans. Internet Inf. Syst. 11(10) (2017)
Silberschatz, A., et al.: Operating System Concepts, 9th edn. Wiley, Hoboken (2016)
Tanenbaum, A., Bos, H.: Modern Operating Systems, 4th edn. Pearson Prentice-Hall, Upper Saddle River (2015)
Stallings, W.: Operating Systems: Internals and Design Principles, 9th edn. Pearson Prentice-Hall, Upper Saddle River (2016)
Ben-Ari, M.: Principles of Concurrent and Distributed Programming, 2nd edn. Addison-Wesley, Boston (2006)
Ben-David, N., Belloch, G.: Analyzing contention and backoff in asynchronous share memory. In: Proceedings of PODC 2017, Washington, DC, USA, 25–27 July 2017 (2017)
Dalessandro, L., et al.: Transcational mutex locks. In: Proceeding of European Conference on Parallel Processing, Italy, 31 August–3 September 2010 (2010)
Trono, J., Taylor, W.: Further comments on “a correct and unrestrictive implementation of general semaphores”. ACM SCIGOPS Oper. Syst. Rev. 34(3), 5–10 (2000)
Hesselink, W.H., IJbema, M.: Starvation-free mutual exclusion with semaphores. Form. Asp. Comput. 25(6), 947–969 (2013)
Udding, J.: Absence of individual starvation using weak semaphores. Inf. Process. Lett. 23, 159–162 (1986)
Friedberg, S.A., Peterson, G.L.: An efficient solution to the mutual exclusion problem using weak semaphores. Inf. Process. Lett. 25, 343–347 (1987)
Wikipedia page. https://en.wikipedia.org/wiki/Promela. Accessed 25 Oct 2017
Gerth, R.: Concise Promela reference (1997). http://spinroot.com/spin/Man/Quick.html. Accessed 25 Oct 2017
Ahrendt, W.: Lecture Slides: Introduction to Promela - in the course Software Engineering using Formal Methods, Chalmers University (2014). cse.chalmers.se/edu/year/2014/course/.../PROMELAIntroductionPS.pdf. Accessed 25 Oct 2017
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Kimm, H., Kimm, H. (2019). Modeling and Verification of Starvation-Free Bitwise Arbitration Technique for Controller Area Network Using SPIN Promela. In: Lee, S., Ismail, R., Choo, H. (eds) Proceedings of the 13th International Conference on Ubiquitous Information Management and Communication (IMCOM) 2019. IMCOM 2019. Advances in Intelligent Systems and Computing, vol 935. Springer, Cham. https://doi.org/10.1007/978-3-030-19063-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-19063-7_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-19062-0
Online ISBN: 978-3-030-19063-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)