An improved HHL Prover: An interactive theorem Prover for hybrid systems

Abstract

Hybrid systems are integrations of discrete computation and continuous physical evolution. To guarantee the correctness of hybrid systems, formal techniques on modelling and verification of hybrid systems have been proposed. Hybrid CSP (HCSP) is an extension of CSP with differential equations and some forms of interruptions for modelling hybrid systems, and Hybrid Hoare logic (HHL) is an extension of Hoare logic for specifying and verifying hybrid systems that are modelled using HCSP. In this paper, we report an improved HHL prover, which is an interactive theorem prover based on Isabelle/HOL for verifying HCSP models. Compared with the prototypical release in [22], the new HHL prover realises the proof system of HHL as a shallow embedding in Isabelle/HOL, rather than deep embedding in [22]. In order to contrast the new HHL prover in shallow embedding and the old one in deep embedding, we demonstrate the use of both variants on the safety verification of a lunar lander case study.