SHF: Small: Automating Improvement of Development Environments for Cyber-Physical Systems (AIDE-CPS)

人们和社会依赖于不同领域的网络物理系统，从交通系统，如汽车和航空航天，到医疗设备。由于这些网络物理系统的安全关键性质，它们的安全和可靠运行至关重要。用于设计网络物理系统的开发工具的可靠和正确运行也至关重要，因为开发工具的缺陷有可能最终导致网络物理系统本身的缺陷。虽然已有广泛的研究努力来解决网络物理系统模型的状态空间爆炸等问题，但在开发方法以确保网络物理系统开发环境的正确性方面投入的努力较少。网络物理系统(CP)的设计和工程流程依赖于大量的构件、模型转换层、编程语言和开发工具，这些通常被认为是正确的，但实际上并非如此。该项目开发了随机差异测试和模糊方法，以在CPS开发环境中自动查找候选缺陷。该项目研究新的正式方法和测试方法，以自动改进CPS开发环境。该框架依赖于三个主要工作：随机生成CPS模型、在不同开发工具之间转换CPS模型、比较CPS模型的动态执行和符号执行。该框架增加了人们对开发环境正确性的信心，这有助于实现网络物理系统的社会效益。

People and society depend on cyber physical systems in diverse domains from transportation systems, such as automotive and aerospace, to medical devices. Due to the safety-critical nature of these cyber-physical systems, their safe and reliable operation is essential. The reliable and correct operation of development tools used to design cyber-physical systems is also vital, since defects in development tools have the capability to culminate in defects in cyber-physical systems themselves. While extensive research efforts exist to address problems such as state-space explosion for models of cyber-physical systems, less effort has been invested in developing methods to ensure correctness of development environments for cyber-physical systems. The design and engineering process for cyber-physical systems (CPS) relies on numerous artifacts, model translation layers, programming languages, and development tools, which are often assumed to be correct but are in fact not. This project develops randomized differential testing and fuzzing methods to automatically find candidate defects in CPS development environments. The project investigates new formal methods and testing approaches to automate improvement of CPS development environments. This framework relies on three primary efforts: randomly generating CPS models, translating CPS models between different development tools, and comparing both dynamic and symbolic executions of CPS models. The framework increases confidence in the correctness of development environments which aids in realizing the societal benefits of cyber-physical systems.