Design and verification by means of model checking of reCANdrv: a media redundancy management driver for the nodes of a ReCANcentrate network

Author David Gessner
Supervisor/s Julián Proenza Arenas | Manuel Alejandro Barranco González
In Universitat de les Illes Balears, 2011.

Controller Area Network (CAN) is a fieldbus widely used in distributed control systems. However, despite its wide use, it is controversial that CAN can be used for systems that require a high level of reliability. This is due to a series of severe dependability limitations of fieldbuses, and in particular of CAN. Nevertheless, many of these dependability limitations can be overcome by replacing their bus topology with a star topology. In particular, ReCANcentrate, a replicated star topology for CAN with advanced error-containment and fault-tolerance mechanisms, overcomes many of these limitations. ReCANcentrate is comprised of two hubs that are coupled with each other and create a single logical broadcast domain. This allows the nodes, which are connected to both hubs, to easily manage the replicated star by means of a software driver called reCANdrv. This driver abstracts away the details of the replication provided by ReCANcentrate and allows a CAN application to communicate with other ReCANcentrate nodes, while tolerating faults and hiding the management of the available redundancy from the application. This paper describes the overall design of reCANdrv and describes the routines that comprise it. Moreover, the paper specifies the properties that a ReCANcentrate node achieves thanks to reCANdrv, and, by creating a model using timed automata implemented using the UPPAAL model checker, verifies that these properties are satisfied by a ReCANcentrate node.

Uso de cookies

Este sitio web utiliza cookies para que usted tenga la mejor experiencia de usuario. Si continúa navegando está dando su consentimiento para la aceptación de las mencionadas cookies y la aceptación de nuestra política de cookies, pinche el enlace para mayor información.