Formal Verification of Control Systems against Hyperproperties via Barrier Certificates.
Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, Majid Zamani · arXiv (Cornell University) · 2021
Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems, such as opacity, robustness, and noninterference, which cannot be expressed using linear time properties. This paper presents a discretization-free approach for the formal verification of discrete-time control systems against hyperproperties. The proposed approach involves decomposition of complex hyperproperties into several verification conditions by exploiting the automata-based structure corresponding to the complement of the original specifications. These verification conditions are then discharged by synthesizing the augmented barrier certificates, which provide certain safety guarantees for the underlying system. For systems with polynomial dynamics, we present a sound procedure to synthesize polynomial-type augmented barrier certificates by reducing the problem to sum-of-squares optimizations. We demonstrate the effectiveness of the proposed approach on two physical case-studies concerning two important hyperproperties: initial-state opacity and initial-state robustness.