Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack

Preprint English OPEN
van Glabbeek, Rob ; Höfner, Peter (2017)
  • Related identifiers: doi: 10.4204/EPTCS.244.2
  • Subject: Computer Science - Logic in Computer Science | Computer Science - Networking and Internet Architecture
    acm: ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS | ComputerApplications_COMPUTERSINOTHERSYSTEMS

We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an in-built mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
  • References (14)
    14 references, page 1 of 2

    [1] T. Bourke, R.J. van Glabbeek & P. Ho¨fner (2014): A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In F. Cassez & J.-F. Raskin, editors: Automated Technology for Verification and Analysis (ATVA '14), LNCS 8837, Springer, pp. 47-63, doi:10.1007/978-3-319-11936-6 5.

    [2] T. Bourke, R.J. van Glabbeek & P. Ho¨fner (2016): Mechanizing a Process Algebra for Network Protocols. Journal of Automated Reasoning 56(3), pp. 309-341, doi:10.1007/s10817-015-9358-9.

    [3] M.J. Dworkin (2007): Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D, National Institute of Standards and Technology (NIST), U.S. Department of Commerce, doi:10.6028/NIST.SP.800-38D.

    [4] K. Etschberger (2001): Controller Area Network: Basics, Protocols, Chips and Applications. IXXAT Automation GmbH.

    [5] A. Fehnker, R. J. van Glabbeek, P. Ho¨fner, A. K. McIver, M. Portmann & W. L. Tan (2012): A Process Algebra for Wireless Mesh Networks. In H. Seidl, editor: European Symposium on Programming (ESOP '12), LNCS 7211, Springer, pp. 295-315, doi:10.1007/978-3-642-28869-2 15.

    [6] R.J. van Glabbeek, P. Ho¨fner, M. Portmann & W.L. Tan (2016): Modelling and Verifying the AODV Routing Protocol. Distributed Computing 29(4), pp. 279-315, doi:10.1007/s00446-015-0262-7.

    [7] H. Krawczyk, M. Bellare & R. Canetti (1997): HMAC: Keyed-Hashing for Message Authentication. RFC 2104 (Informational, Errata Exist). Available at http://tools.ietf.org/html/rfc2104.

    [8] T. Nipkow, L. C. Paulson & M. Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer, doi:10.1007/3-540-45949-9.

    [9] Robert Bosch GmbH, Stuttgart, Germany (1991): CAN Specification, Version 2.0. Available at http://www. bosch-semiconductors.de/media/ubk_semiconductors/pdf_1/canliteratur/can2spec.pdf.

    [10] C. Shin (2014): A framework for fragmenting/reconstituting data frame in Controller Area Network (CAN). In: International Conference on Advanced Communication Technology (ICACT '14), IEEE, pp. 1261-1264, doi:10.1109/ICACT.2014.6779161.

  • Metrics
    No metrics available
Share - Bookmark