bCANDLE: Formal modelling and analysis of CAN control systems

David Kendall, Steven Bradley, William Henderson, Adrian Robson

Research output: Contribution to conferencePaperpeer-review

4 Citations (Scopus)

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.
Original languageEnglish
DOIs
Publication statusPublished - 1998
EventFourth IEEE Real-Time Technology and Applications Symposium - Denver, CO
Duration: 1 Jan 1998 → …

Conference

ConferenceFourth IEEE Real-Time Technology and Applications Symposium
Period1/01/98 → …

Fingerprint Dive into the research topics of 'bCANDLE: Formal modelling and analysis of CAN control systems'. Together they form a unique fingerprint.

Cite this