| EPSRC Reference: |
EP/E021948/1 |
| Title: |
Resource Analysis and Verification for Dependable Embedded Software |
| Principal Investigator: |
Qin, Professor S |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Durham, University of |
| Scheme: |
First Grant Scheme |
| Starts: |
01 February 2007 |
Ends: |
31 July 2010 |
Value (£): |
213,681
|
| EPSRC Research Topic Classifications: |
| Software Engineering |
System on Chip |
| VLSI Design |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
In recent years, embedded systems have become ubiquitous in our daily life. They are widely built into home electrical appliances, such as washing machines, microwave ovens, dryers and dishwashers. They also exist in mobile devices like PDAs, navigators, mobile phones and smart cards, making our life more convenient and enjoyable. In addition, they are often used in safety critical systems such as military units, medical devices and motor cars. These embedded systems are often supplied with limited memory and computation resources due to various constraints on e.g. product size, power consumption and manufacture cost. Paying insufficient attention to resource issues when developing software for such systems may result in a corresponding software failure after deployment. A real example is the anamoly problem of the Mars Rover Spirit which was due to a memory leakage problem ignored in the software development process. In some cases, such software failure may put human lives at risk. It is thus very important to ensure resource safety and guarantee resource performance for embedded software. We propose to study resource safety and performance for object-oriented (OO) programs running on embedded devices. One aim of our proposed research is to predict statically (i.e. before a program starts to run) and precisely the memory performance of embedded software and to ensure that such software will never require more memory than the device can provide. In addition to memory resource, we will also study timing performance of embedded software which is also of great importance in real-time embedded system design. We intend to develop type-based static analysis techniques to verify memory safety and performance. More specifically, we will keep track of symbolic sizes of data structures which are then used to analyze and infer the memory usage bounds statically (i.e., at compile-time). As a simple example, when a piece of code is about to be downloaded into a mobile phone, our system will be able to check whether the program requires more memory than the phone can provide. We will also develop enhanced region-based memory management mechanisms to improve the overall memory performance of OO programs, where stack-allocated regions will be guided by a symbolic size analysis. This sized-region mechanism is very useful for real-time applications as it can prevent unbounded interference caused by garbage collection. We will also extend our symbolic size analysis to software timing analysis so as to achieve tighter prediction on worst case execution time of OO programs. Based on our research outcomes, we will build a resource analysis and verification tool for embedded software. We believe a more precise resource analysis can help us verify resource safety and possibly tune certain resource-unsafe programs to safe ones. Moreover, it can provide us with an opportunity to reduce the cost of end-user embedded products. This is so as a tighter worst-case execution time would indicate a possibility of using a slower (thus cheaper) hardware processor/device, and a tighter memory usage prediction would suggest that further reduction can be made to the memory footprint to save on hardware size and probably power consumption. We believe a thorough and precise resource analysis would help build more dependable embedded software. Our research outcomes would provide a foundation for building systems with limited resource constraints in a reliable and efficient way.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
|