Compositional Verification of Hybrid Systems

Jump to: navigation, search

Technical point of contact: Brandon Hencey, AFRL
Period of activity: 2016-2019

Overview of the Project

The objective of this project is to develop theory and algorithms for the compositional verification of control protocols for systems governed by hybrid dynamics.

Contract-based reasoning roughly refers to establishing certificates on the behavior of the (entire) system from independently established certificates (also known as assume-guarantee specifications) for its components. It facilitates modularity and changes in the system because, even if the individual components or their controllers change, the certificate for the composite system is preserved as long as the replacement---either at design or run time---satisfies its local certificate. Furthermore, it also provides a basis to mathematically instantiate so-called open system architectures. We propose a compositional framework for verification of systems that are formed as interconnection of multiple subsystems. The method constructs certificates of input-output properties of subsystems in isolation from other subsystems and assembles certificates for the interconnected system based on these subsystem certificates. The assembly of system-level certificates from subsystem certificates, of course, has to account for the fact that the output of a subsystem is the input of another subsystem (i.e., for the interconnection structure). The proposed effort will instantiate such contract-based reasoning methods---and systematic search for subsystem components---to systems whose subsystems are modeled as hybrid systems.