SBIR Phase I: Runtime Verification for Automobiles

The broader impact/commercial potential of this Small Business Innovation Research (SBIR) Phase I project is that it will offer the automotive industry higher reliability from the software systems powering automobiles, by enabling runtime monitoring while providing the maximum possible correctness guarantees for the generated monitors. Cars will be safer and more rigorously assured. This project will address a slew of recent problems with software failures, security compromises, and other unintentional software behaviors that occur inevitably as systems become more complex, potentially saving lives and making millions of vehicles safer, easier to upgrade, and better tested. The commercial value follows the need of manufacturers to retain the basic vehicle safety guarantees while pursuing the commercial necessities of competing on complex software-driven features, ultimately minimizing software development costs and expensive car recalls. The enhanced scientific and technological understanding from this technology will come as it is deployed in the field, giving manufacturers an impetus to formalize and standardize existing requirements, bolstering their understanding of the software systems in the car. The technology will also foster the formalization of both open and proprietary specifications, further increasing the understanding of complex automotive systems by facilitating complete analysis. This Small Business Innovation Research (SBIR) Phase I project will for the first time explore the application of provably correct runtime verification software to real-time systems. An efficient and certifying framework allowing for the expression of a diverse range of specifications will enable applications of runtime verification in automobiles, aeronautics, and beyond. One research objective is to develop a system that can monitor any safety property, generating high-performance C code capable of running on virtually any hardware. This will combine efficient monitoring with maximal formal guarantees in terms of correctness. Formal verification was previously realized only for mathematical models of monitors, or in systems with very low expressiveness. A second research objective is to study the applicability of runtime verification by collecting properties from automotive industry standards, evaluating the complexity of specifying the properties, the possibility of recovering from detected violations, and the performance requirements of the resulting monitors. It is anticipated that hundreds or even thousands of such properties will be monitored simultaneously.