CPS: Small: Software-State Observability in CPS

自动化飞机和汽车等计算机物理系统(CPS)技术已经变得足够复杂，以至于CPS软件验证现在成为产品开发的主要瓶颈。这个项目研究了自动生成CPS软件简化模型的新方法，以便将这些模型纳入分析，例如，在系统范围的模拟或错误检测中。该项目将允许CPS软件与最先进的方法相比更灵活地进行适配和分析，最先进的方法通过禁止使用许多现代编程构造和惩罚设计过程中迭代的软件改进来限制软件开发人员。该项目的智力优势是引入了软件状态可观测性理论，这将对CPS分析具有广泛的实用价值，包括在线错误检测等应用。为此，该项目集中于三个具体目标：(I)基于对CPS软件程序的静态和动态分析，开发用于降阶软件建模的概念；(Ii)提出软件状态可观测性理论，以使得能够跨越物理和软件组件的边界进行状态估计；以及(Iii)将这些理论应用于开放源代码飞行控制系统的在线错误监测。该项目与在CPS中对软件的传统处理方式有根本的不同，在CPS中，必须事先严格地指定软件，其中必须仔细地验证程序以证明其符合规范，并且在最终验证之后，该软件被认为基本上没有错误。我们的方法允许开发人员在创建新的CPS软件时拥有更大的自由度，要求合理但不过度的初始测试，这一点得到了更好的分析工具和在线可靠性监测的支持。其结果将使自动化汽车和无人驾驶飞机变得更复杂、成本更低。与该项目相关的成果将通过档案出版物共享，数据将通过塔夫茨大学https://tufts.box.com/s/aq305785bg2s3j29lls8u4wdpybzpcth.在线提供上传到此存储库的软件将在适当的许可模式(如BSD或APACHE)下可用。数据将至少在整个项目期间被保留。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

Cyber-physical system (CPS) technologies, such as automated aircraft and cars, have become sufficiently complex that CPS software verification is now a major bottleneck in product development. This project examines new approaches for auto-generating reduced models of CPS software, in order to incorporate those models in analysis, for instance, in system-wide simulations or bug detection. This project will allow CPS software to be adapted and analyzed much more flexibility in comparison with state-of-the-art methods, which limit software developers by prohibiting use of many modern programming constructs and by penalizing iterative software improvements during the design process.The project's intellectual merit is the introduction of a theory of software-state observability, which will have wide utility for CPS analysis including in applications such as online bug detection. To this end the project concentrates on three specific aims: (i) the development of concepts for reduced-order software modeling based on static and dynamic analyses of CPS software programs, (ii) the formulation of a theory of software-state observability to enable state estimation across the boundaries of physical and software components, and (iii) the application of these theories to online bug monitoring for an open-source flight control system.The project represents a fundamental departure from the conventional treatment of software in a CPS, where software must be tightly specified in advance, where the program must be carefully verified to prove that it meets specifications, and where after final validation the software is assumed to be essentially free of bugs. Our approach permits developers much greater latitude in creating new CPS software by requiring reasonable but not excessive initial testing, as justified by better analysis tools and by online reliability monitoring. The result will enable more sophisticated and lower cost automated cars and unmanned aircraft. Results related to the project will be shared through archival publications and data will be made available online through Tufts University at https://tufts.box.com/s/aq305785bg2s3j29lls8u4wdpybzpcth. Software uploaded to this repository will be available under suitable licensing models (such as BSD or Apache). Data will be retained at least through the duration of this project.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.