Skip to main content


Split, send, reassemble: A formal specification of a CAN bus protocol stack


Rob van Glabbeek and Peter Hoefner




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.

BibTeX Entry

    publisher        = {Open Publishing Association},
    doi              = {10.4204/EPTCS.244.2},
    author           = {van Glabbeek, Robert and H\"ofner, Peter},
    month            = mar,
    editor           = {{H. Hermanns and P. H\"ofner}},
    year             = {2017},
    keywords         = {can bus, fragmentation protocol, priority inversion, process algebra, awn.},
    title            = {Split, Send, Reassemble: A Formal Specification of a {CAN} Bus Protocol Stack},
    booktitle        = {2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)},
    pages            = {14--52},
    address          = {Uppsala, Sweden}


Served by Apache on Linux on seL4.