SHF: Small: A Hybrid Synchronous Language for Verifiable Execution of Cyber-Physical Systems

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

Modern cyber-physical systems (CPSs) such as cars and aircraft are responsible for expensive equipment and human lives. To ensure that they operate in a safe manner, it is therefore important to formally verify the underlying code. However today, tools for verification, execution and simulation of cyber-physical systems are largely disconnected, and difficult to reconcile. As a result, formal verification often ends up verifying a model of the code rather than the code that is actually executed, creating a gap in the verification. The project creates MARVeLus, a programming language unifying verification, execution and simulation of cyber-physical systems. The project's novelties are to bridge the gap between verification, execution and simulation, to offer a methodology for end-to-end verification of cyber-physical systems, and to ensure that the code that is executed is also the code that was verified. The project's impacts are to empower tomorrow's engineers to design cyber-physical systems with strong, formally verified guarantees applicable to real-world systems, and to democratize the use of formal verification in the design of cyber-physical systems. The investigator maintains strong ties with industry, which facilitates industry evaluation and feedback. The project also includes a collaboration with a Detroit-area Title 1 middle school to make the students aware of safety issues in engineering. The difficulty to achieve verification, execution and simulation together stems from multiple fronts: the intricacies of the semantics of languages for cyber-physical systems, including machine arithmetic; the complication of modeling and communicating with sensors and actuators; and the challenges in accurately modeling, simulating and proving properties about continuous dynamics, especially when coupled with discrete programs. To resolve those challenges, the project models cyber-physical systems as hybrid systems, with both discrete and continuous dynamics. MARVeLus is first designed as a synchronous language, in the tradition of languages such as Lustre, Esterel and Signal. Synchronous languages are stream-based languages built around a synchronous clock and targeted to cyber-physical systems and embedded systems. They come with strong runtime and memory guarantees. By building MARVeLus on a synchronous platform, we leverage their success based on decades of research, and encourage industry adoption. Second, MARVeLus enables verification through refinement types and an external Satisfiability Modulo Theories (SMT) solver. The project builds a dedicated refinement type system to reason about different properties of hybrid systems, including safety and liveness. Third, the project adds ordinary differential equations to the synchronous language, inspired by the recent development of the synchronous language Zelus. The project builds refinement typing rules allowing the user to reason about those differential equations using explicit solutions and invariants. Finally, the project performs verified simulation by formally verifying numerical algorithms approximating differential equations, and formally bounding their errors. As a result, MARVeLus is a synchronous language with differential equations and refinement types, with a verified simulation capability. The project applies and evaluates the design of MARVeLus on a small ground robot and a quadcopter in the laboratory, on the industrial aircraft collision avoidance system ACAS X. 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.