Search papers, labs, and topics across Lattice.
This paper formalizes the operational semantics of hybrid synchronous programs, including initial value problems and zero-crossing detection, to enable formal verification of CPS software. They extend the type system of a synchronous programming language with refinement types to verify hybrid behavior and prove the soundness of this extended type system. This allows for verification of executable controller code against precise models of the environment in a wider variety of cyber-physical systems.
Guaranteeing safety in autonomous systems gets a boost: this work enables formal verification of hybrid system code that directly controls physical processes.
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.
