Design and Verification of a Media Redundancy Management Driver for a CAN Star Topology

Some of the severe dependability limitations of Controller Area Network (CAN) can be overcome by replacing its bus topology with a star topology. Thus, a replicated star topology with advanced error-containment and fault-tolerance mechanisms for CAN, called ReCANcentrate, has been proposed. Its two hubs are coupled with each other and create a single logical broadcast domain. This allows each node to easily manage the replicated star by means of a software driver, called reCANdrv, that abstracts away the details of this replication. The goal of reCANdrv is to manage the star's media redundancy transparently for a CAN application, allowing it to exchange information through the star while tolerating faults. This paper describes the design of reCANdrv, the specification as properties of reCANdrv's correct redundancy management, and the verification of these properties by means of model checking.