Automated Revision of Embedded Systems

Principle Investigator: Sandeep Kulkarni

Funding from: AFOSR

Proposal Summary

This project focuses on automated program revision of programs where an existing program is to be transformed to meet new properties of interest. Need for such revision arises in several scenarios, e.g., when the requirements change, or bugs are found. We consider program revision for cases where an existing program is modified to meet new safety properties, new timing constraints, and/or new fault-tolerance requirements. One of the important requirements for such revision is that no new bugs are introduced during the revision, i.e., existing properties continue to be satisfied.

With this motivation, in this project, we will develop complexity results, algorithms and tools for automated program revision for embedded systems, which are engineering artifacts that involve computation that is subject to physical world constraints. In particular, we will focus on three main challenges in such program revision: First, we will develop complexity results and algorithms for the case where the program needs to satisfy real-time constraints with partial observability caused due to the fact that one component cannot observe the internal state of another component. Second, we will develop models and algorithms for representing the constraints imposed by the fact that the embedded system has to interact with the physical world. Third, we will develop algorithms for providing graceful degradation, a property crucial for embedded systems employed in safety critical systems. We will also integrate the algorithms developed in this proposal with our synthesis tool SYCRAFT. We expect that this will assist in designers to perform automated revision to satisfy new properties in embedded programs as well as to find missing specifications.