Overview

David Kendall led the High Integrity Embedded Systems Group at Northumbria University in the 1990s. The group conduct research into formal methods in the engineering of embedded systems, in particular the application of model-checking in the design and analysis of real-time systems.

He is the main architect of CANDLE, a modelling language and development environment for distributed embedded systems built using the Controller Area Network (CAN). He was previously involved in the AORTA project. He is the author or co-author of a number of academic publications (see his Google Scholar Profile).

Embedded Systems

Embedded control systems appear in many of the manufactured products upon which our society increasingly depends, from household goods such as washing machines and video recorders to advanced space vehicles or nuclear power plant controllers. In every case, 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 industrial sectors where reliability is paramount, such as transport, medical, chemical and manufacturing.

My research is concerned with the theory and practice of embedded systems development and analysis. In particular, I am interested in the key concepts and advanced practical techniques and tools required for the production of embedded systems solutions which are

high-integrity,
real-time,
distributed, and
open.

Projects

CANDLE

The project is concerned in particular with the Controller Area Network (CAN) protocol which is a de facto standard in the automotive industry. An abstract formal model of CAN is developed. This model is adopted as the communication primitive in a new language, bCandle, which includes value passing, broadcast communication, message priorities and explicit time. A high-level language, candle, is introduced and its semantics defined by translation to bCandle. We show how realistic CAN systems can be described in candle and how a timed transition model of a system can be extracted for analysis. Most importantly, it is shown how efficient methods of analysis, such as `on-the-fly' and symbolic techniques, can be applied to these models.

See also The CANDLE project has its own page on the VASY site at INRIA.

AORTA

The AORTA project was concerned with the development of a formal language for the development of small, multi-tasking embedded systems implemented on uni-processors, employing a simple scheduling algorithm. It was one of the first projects ever to consider both the implementation and verification of asynchronous, hard real-time systems.

Research students

Neil Eliot Energy-efficient swarming protocols for UAVs, 2017
Stephen Doswell Anonymity and mobility in IP networks, 2015
Ali Almohammad Rigorous code generation for distributed embedded systems, 2012
Michael Brockway, Compositionality in the formal modelling and analysis of broadcasting embedded control systems, 2010
Kashif Saghar, Formal modelling and analysis of denial of service attacks in wireless sensor networks, 2010
Stephen Bradley, An implementable formal language for real-time systems, 1995
David Turner, Predictable communication protocols for real-time systems, 1995