CANDLE Language and Environment for CAN Control Systems

Organisation:	Northumbria University (UNITED KINGDOM)
Functionality:	High-level language and development environment for CAN control systems.
Tools used:	OPEN/CAESAR
Period:	2001
Description:	CANDLE is a high-level programming language and development environment for control systems implemented using the Controller Area Network (CAN) communication protocol. It is designed to integrate the production of a CAN system implementation and its formal model. CAN provides multi-master, priority-based bus access based on a CSMA/CR protocol whose deterministic collision resolution policy makes it suitable for use in hard real-time systems. Use of CAN is widespread in the automotive industry and in other sectors where the requirement for high assurance systems provides a strong incentive for the application of formal development methods. A CANDLE program consists of a high-level description of the behaviour of system processes and the structure of the network via which they communicate. The control of a system model is represented as a timed Petri net, derived automatically by translation from the CANDLE program, which has the advantage of giving a compact representation of the control aspects of the system. In previous approaches, this Petri net was translated into a timed automaton and analysed using existing model checkers (e.g., KRONOS). However, these approaches suffer from a number of disadvantages, the most serious being that they allow the generation of redundant locations and edges and can produce extremely large timed automata. In the current approach, the Petri net is translated into a simulation graph, in which time information is represented using clock zones. The simulation graph is represented by a C program implementing the OPEN/CAESAR graph API, which is automatically generated from the timed Petri net. This program provides functions for generating the initial simulation graph node and iterating over the simulation graph successors of a node. This program also implements on the fly the well-known clock activity abstraction technique. The simulation graphs of a number of examples have been generated. In each case, the simulation graph with clock activity reduction is several orders of magnitude smaller that the corresponding timed automaton. In one case, it was not even possible to generate the timed automaton, whereas the simulation graph with clock activity reduction was easily generated.
Conclusions:	The general approach of translation from a high-level language through a number of intermediate stages to C source code implementing the OPEN/CAESAR API has proved to lead to an effective decomposition of the translation problem, providing opportunities for optimisation at every stage and resulting in programs which can be connected easily with a variety of analysis tools. This approach clearly outperforms methods in which a timed automaton is constructed explicitly.
Publications:	[Kendall-01-a] David Kendall. "CANDLE: A tool for efficient analysis of CAN control systems". Proceedings of the 1st Workshop on Real-Time Tools RT-TOOLS'2001 (Aalborg, Denmark), Technical Report of University of Uppsala number 2001-014, August 2001. Available on-line at: http://computing.unn.ac.uk/staff/cgdk2/publications/rttools01.ps.gz or from the CADP Web site in PDF or PostScript [Kendall-01-b] David Kendall. "Formal Modelling and Analysis of Broadcasting Embedded Control Systems". PhD thesis, University of Newcastle upon Tyne, Department of Computing Science, September 2001. Available on-line at: http://computing.unn.ac.uk/staff/cgdk2/publications/ken01.ps.gz or from the CADP Web site in PDF or PostScript
Contact:	Dr. David Kendall Northumbria University School of Informatics Pandon Building Camden Street Newcastle upon Tyne NE2 1XE United Kingdom Tel: +44 (0)191 2437619 Fax: +44 (0)191 227 3662 Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page