Design and formal verification of a fault-tolerant clock synchronization subsystem for the controller area network

Abstract

[cat] Controller Area Network (CAN) és un bus de camp amplament utilitzat dins l’àrea dels sistemes encastats distribuïts. S’ha documentat que per tal de fer CAN vàlid per aplicacions amb garantia de funcionament, és necessària la provisió d’un servei adequat de sincronització de rellotge; on l’adequació es mesura en funció de tres atributs: alta precisió, tolerància a fallades i baix cost. Aquesta tesi aborda el disseny i l’avaluació formal d’una nova solució per sincronització de rellotge sobre CAN que tracta aquests tres aspectes satisfactòriament. Aquesta solució s’implementa en hardware, utilitza un esquema mestre/esclau i rep el nom de Orthogonal Clock Subsystem for CAN (OCS-CAN). L’avaluació formal dels mecanismes de tolerància a fallades d’OCS-CAN s’ha fet analíticament i també mitjançant model checking i autòmats temporitzats. Això ha requerit el desenvolupament d’unes tècniques específiques de modelització que són aplicables a un ample ventall de sistemes encastats distribuïts amb rellotges.

[eng] The Controller Area Network (CAN) is a fieldbus extensively used in the area of distributed embedded systems. It has been reported that, in order to make CAN adequate for dependable applications, the provision of a suitable clock synchronization service is required; where suitability is measured in terms of three attributes: high precision, fault tolerance and cost effectiveness. This thesis discusses the design and formal assessment of a novel solution for clock synchronization over CAN that addresses these three aspects with satisfactory results. This solution is hardware-implemented, uses a master/slave scheme for synchronization and is called the Orthogonal Clock Subsystem for CAN (OCS-CAN). The formal assessment of the fault tolerance mechanisms of OCS-CAN is performed both analytically and by means of model checking and timed automata, and it has required the development of specific modeling techniques that are applicable to a wide range of distributed embedded systems with computer clocks.