bCANDLE: Formal modelling and analysis of CAN control systems

Embedded control systems appear in many of the manufactured products upon which our society increasingly depends. System developers need better development methods in order to be more confident that the systems which they deliver will behave properly. The need is particularly pressing in the case of distributed, hard real-time control systems for which testing is notoriously difficult. In recent years, much research has been conducted into formal techniques for analyzing the quantitative temporal properties of system models. Such work offers the promise of complementing testing in the validation of systems by approaches which include simulation, symbolic monitoring, assertion checking and verification. The principal contribution of this paper is the introduction of a modelling language, bCANDLE, whose intended domain comprises embedded control systems in which computing nodes communicate using one or more Controller Area Networks (CAN). bCANDLE is a simple but expressive language which includes value passing broadcast communication, message priorities and an explicit time construct. In giving a formal semantics to bCANDLE in terms of timed transition systems, we present for the first time an abstract, timed formal model of CAN.