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.