Recently there has been great progress in improving software reliability through automatic techniques for detecting software errors (i.e., bugs). This project builds on this recent work to address problems of reliability in embedded software. While in some respects embedded software is similar to all other complex software systems (e.g., many embedded software systems build on standard libraries) in other respects embedded software is different. Some of the characteristic features of embedded software systems are: ubiquitous use of concurrency and distribution, the central role of continuous control laws to model and predict behavior in the physical world, real-time requirements, and often very limited computational resources. The project expects to make significant advances by focusing specifically on error detection and verification for just such aspects of embedded software. The methodology is to study an existing, ongoing embedded software project, which initially is the Stanford Autonomous Car. Through experimentation and interaction with the team building the Autonomous Car, partial specifications are being developed that can be checked by the tools developed in the project.
Modern software systems are incredibly complex and prone to failure in very complex ways. Embedded software systems increasingly control the physical infrastructure of society (hospitals, power plants, dams, and so on) and thus the cost of software failures becomes greater with the passage of time. Automatic software analysis is one of the most promising avenues to improving software quality; the focus of this project is to apply these ideas to the unique aspects of embedded software. If successful, this project will make significant advances in the ability to analyze and predict the behavior of embedded software systems.
