by Kevin Hammond
The EU-funded EmBounded project aims to develop new techniques for providing formal guarantees on resource usage bounds. It is a collaborative project between AbsInt GmbH, a high-tech company specialising in high integrity real-time systems, and academic partners in the UK, France and Germany.
A major difficulty with constructing embedded systems is that the available system resources (processor, computer memory, power) are necessarily restricted due to cost and other considerations. If it were possible to determine strong bounds on the use of such resources, then potentially there would be significant benefits in terms of manufacturing cost, reliability and performance. However, determining such bounds automatically is a difficult problem and doing so manually is becoming impracticable as embedded software increases in complexity.
The EmBounded project, led by Dr Kevin Hammond at the University of St Andrews, aims to research this problem. Our vision is one where certificates of the bounds on resource usage can be obtained from a source program, through automatic program analysis, independently of the usual software compilation process. These certificates may then be verified using formal proof techniques based on a program logic that captures the meaning and behaviour of programs.
The EmBounded project builds on European strengths in programming language design, program analysis and embedded applications. Our work is based around a new domain-specific programming language notation, Hume, that aims to find an optimum point between good programming abstraction and the ability to derive good cost information. Hume embeds a rule-based notation for sequential computations within a finite-state-machine-based notation for concurrency control. The process notation is designed to be easily tractable to standard analyses such as model-checking for deadlock detection; while the rule-based notation is designed so that we can easily expose information about cost. Hume is designed to be practical as well as having interesting language properties. Prototype implementations of Hume produced at Heriot-Watt University can run in less than 30KB on a standalone Renesas M32C development board, with minimal dynamic memory requirements, depending on the end-application.
To date, project researchers at Ludwig-Maximilians-Universität, München, and St Andrews University have developed new theoretical models of bounded resource usage for dynamic memory and time metrics based on Hume program source. They have related these formally to the underlying machine operations using an abstract-machine approach. We are now constructing automatic analyses based on these models that will expose resource constraints and other program properties in our program logic. This will give a good model of program cost based on the program structure.
In order to obtain accurate information about time usage on a specific computer architecture, we are using the aiT tool developed by AbsInt GmbH to provide precise and guaranteed timing costs for fragments of machine code programs. This low-level information can then be combined with the high-level information obtained from our program source to provide a highly accurate analysis that will give guaranteed bounds on program execution time.
In order to produce convincing results, it is necessary to test our approach using sophisticated and realistic applications. Researchers at the Laboratoire des Sciences et Matériaux d'Électronique - LASMEA (Clermont-Ferrand, France), have been developing a number of real-time computer vision algorithms in Hume. These algorithms can be exploited to detect, for example, road features from a moving vehicle, an essential component of any self-controlled (autonomous) road vehicle. In due course, we intend to apply these algorithms to the sensor and control systems used in the CyCab autonomous vehicle (http://www.robosoft.fr), a self-controlled electric car resembling a golf buggy, and capable of speeds up to a rather alarming 30 km/h.
Links:
Project: http://www.embounded.org
Hume: http://www.hume-lang.org
Please contact:
Kevin Hammond, University of St Andrews, Scotland, UK
E-mail: kh
dcs.st-and.ac.uk
