Computer performance has doubled many times over during the past 40 years, but the very techniques used to achieve these performance gains have made it increasingly difficult to build systems that are provably safe, secure, or reliable. This fact significantly impedes progress in the development of our most safety-critical embedded systems such as those found in medical, avionic, automotive, and military systems. A transformation in the way that these systems are created is needed, one that uses new hardware design techniques, computer architectures, and programming languages to create classes of hardware/software systems with formal and provable safety properties that are verifiable all the way down to the implementation level of bits and logic gates.
This research will change the way that hardware and embedded systems designers approach the problem of provable properties, enabling them to directly control and analyze the system at the lowest level and to statically determine if their designs are in compliance with a given policy. For example, if a system must be real-time this property can be verifiable for a full system, from gates to software, by ensuring that the architecture design carefully manages interference through a set of new hardware primitives, software designed to exploit these new primitives, specialized hardware analysis tools, and new design languages. To ensure this technology will have impact beyond academia the PIs are making these new technologies available and accessible through easy to use tools, continuing to include undergraduates at all levels of research to help train a new generation of engineers capable of designing safety-critical systems, and integrating concepts from information assurance into their extensive outreach activities. Over the long term this research will help create the skills and tools that embedded system engineers need to evaluate the trustworthiness of their systems, and it will ease the development of those critical systems on which we all depend on for our safety and livelihood.
