SBIR Phase I: Runtime Verification for Automobiles

这个小型企业创新研究(SBIR)第一阶段项目的更广泛的影响/商业潜力是，它将通过启用运行时监控，同时为生成的监视器提供最大可能的正确性保证，从驱动汽车的软件系统向汽车行业提供更高的可靠性。汽车将变得更安全、更有保障。该项目将解决最近出现的一系列软件故障、安全漏洞和其他无意软件行为问题，这些问题随着系统变得更加复杂而不可避免地出现，有可能挽救生命，并使数百万辆汽车更安全、更容易升级和更好地测试。商业价值源于制造商需要保留基本的车辆安全保证，同时追求在复杂的软件驱动功能上竞争的商业必要性，最终将软件开发成本和昂贵的汽车召回降至最低。随着这项技术在现场的部署，人们对这项技术的科学和技术理解将会增强，这将推动制造商将现有需求正式化和标准化，从而加强他们对汽车软件系统的理解。该技术还将促进开放和专有规范的形式化，通过促进完整的分析进一步增加对复杂汽车系统的理解。这个小型企业创新研究(SBIR)第一阶段项目将首次探索将可证明正确的运行时验证软件应用于实时系统。允许表达各种规范的高效和认证框架将使运行时验证在汽车、航空和其他领域的应用成为可能。其中一个研究目标是开发一种可以监控任何安全属性的系统，生成能够在几乎任何硬件上运行的高性能C代码。这将在正确性方面将有效的监测与最大限度的正式保证结合起来。以前，正式验证只针对监视器的数学模型，或者在表现力非常低的系统中。第二个研究目标是通过从汽车行业标准收集属性、评估指定属性的复杂性、从检测到的违规中恢复的可能性以及由此产生的监视器的性能要求来研究运行时验证的适用性。预计将同时监测数百甚至数千个这样的财产。

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.