bCANDLE: Formal modelling and analysis of CAN control systems

Kendall, David, Bradley, Steven, Henderson, William and Robson, Adrian (1998) bCANDLE: Formal modelling and analysis of CAN control systems. In: Fourth IEEE Real-Time Technology and Applications Symposium, 3-5 June 1998, Denver, CO.

Full text not available from this repository. (Request a copy)

Abstract

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.

Item Type:	Conference or Workshop Item (Paper)
Subjects:	H600 Electronic and Electrical Engineering
Department:	Faculties > Engineering and Environment > Computer and Information Sciences
Depositing User:	Becky Skoyles
Date Deposited:	16 Feb 2015 15:10
Last Modified:	13 Oct 2019 00:24
URI:	http://nrl.northumbria.ac.uk/id/eprint/19002

Downloads