Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

TL;DR

This paper advances formal verification methods for hybrid synchronous programs, enabling precise modeling and verification of complex cyber-physical systems with differential equations.

Contribution

It formalizes the semantics and extends the type system of a synchronous language for hybrid systems, proving its soundness.

Findings

Formal semantics of initial value problems established

Type system extended for hybrid verification

Soundness of the extended type system proven

Abstract

Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of certainty. Formal verification has been employed to verify the software controlling these systems, but due to their complexity, is usually performed on an abstract model rather than the executable code. Synchronous programming languages extended with differential equations promise both rigorous modeling and sufficient expressiveness to implement executable controller code, and recent developments have introduced formal verification of strictly discrete-time programs. Extending these verification techniques to hybrid systems enables precise modeling of the environment for a wider variety of programs to be both verified and executed. We formalize the operational semantics of initial value problems and zero-crossing detection expressed in a synchronous programming language, extend its type system for verification thereof, and prove its soundness.