FMitF: Track II: Hybrid and Dynamical Systems Verification on the CPS-VO

点击翻译按钮获取中文摘要

This project aims to transition recent research results that automate portions of the verification process of Cyber-Physical Systems into broader practice, particularly with industrial and student users. Cyber-physical systems (CPS) are networked embedded computing systems coupled with physics, such as in motor vehicles, aircraft, medical devices, and the electrical grid. Due to their frequent use in safety-critical scenarios where significant losses may be incurred, such as of human life or monetarily, the engineering process for such systems devotes vast resources to the process of verification to ensure these systems meet their requirements. The approach builds upon recent successes in the hybrid systems verification competition (ARCH-COMP) hosted in the past three years, in which several dozen hybrid systems verification tools have competed across several problem and system categories. To achieve the transition of verification research results for CPS models into broader practice, this project develops a cloud-based framework to interface with and execute state-of-the-art formal verification software tools from the hybrid and dynamical systems verification community using NSF's CPS Virtual Organization (CPS-VO). The project extends the Design Studio and Tool Integration frameworks for the CPS-VO, to provide an easy-to-use interface for these verification tools. It also serves as a repository for housing executable versions of the tools and benchmarks, plus facilitating repeatability evaluations for ARCH-COMP through a distributed, cloud-based execution architecture. The core technology upon which the tool is built is the hybrid systems model source transformation and translation (HyST) software tool, which performs semantics-preserving translation between state-of-the-art hybrid systems verification tools.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.