People and society depend on cyber­-physical systems (CPS) 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 relies on numerous artifacts, model translation layers, programming languages, and development tools, which are often assumed to be correct, but like any software, may have defects and bugs in them.

This project developed randomized differential testing and fuzzing methods to automatically find candidate defects in cyber-physical systems development environments. The project developed new formal methods and testing approaches to automate improvement of cyber-physical systems development environments. This framework relied on three primary efforts: randomly generating cyber-physical systems models, translating cyber-physical systems models between different development tools, and comparing both dynamic and symbolic executions of cyber-physical systems models. The framework increases confidence in the correctness of development environments to aid in realizing the societal benefits of cyber­physical systems.

For intellectual merit, the primary outcomes of the project include several publicly available software frameworks implementing the core ideas for identifying defects in cyber-physical systems development environments, specifically SLEMI, SLForge, CyFuzz, HyST, and HyRG. SLEMI, SLForge, and CyFuzz integrate with the MathWorks' Simulink cyber-physical systems development environment, and together have identified around two dozen confirmed bugs/defects in these industry-grade tools used in the cyber-physical systems development process. The HyST and HyRG tools have been used to perform model transformation between different formal representations of cyber-physical systems models, and together have identified defects/bugs in several hybrid systems model checkers. Together, these testing environments have served to improve the reliability of existing cyber-physical systems development environments, and the underlying intellectual techniques may improve the testing process for future development tools, as illustrated in part with the project participants' engagement with the MathWorks and their Simulink development environment.

For broader impacts, this project also was essential in the development of the first three iterations in 2017, 2018, and 2019, of the hybrid systems verification competition (ARCH-COMP) held in conjunction with the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH), in which a broad swath of the cyber-physical systems verification community participated (increasing from around a dozen participants in 2017 to over three dozen in 2019).

Last Modified: 12/03/2019
Modified by: Taylor T Johnson