ITR: Formal Methods for Robust Embedded Software

University Of Utah, Salt Lake City UT

Investigators

Abstract

To overcome the limitations of current development methods for embedded software, which include limited use of secure and type-safe languages and the lack of support for formal validation techniques, this work explores the use of the modern secure language Java coupled with light-weight formal methods to establish correctness. It tailors the Java technology to fit the domain of embedded systems by placing restrictions on the Java subset, supporting provably correct-by-construction synthesis techniques for reactive control skeletons, and analysis techniques based on algorithmic as well as deductive formal verification techniques. A key goal is also to support advanced features such as dynamic software upgrades and process migration through safe implementation methods that are formally verified. It develops a new set of model-checking and program analysis tools that are demonstrated on prototype hardware/software co-designs of embedded Java processors.