Compositional verification of complex systems is a challenging problem. We developed two new approaches to enable compositional analysis of continuous and hybrid dynamical systems: a
certificate-based approach and an approach based on computing
relational abstractions.
The certificate-based approach directly searches for certificates of correctness using constraint solving. Certificates vary depending on the property. This approach can be used to create assume-guarantee contracts for open components. It requires templates for the form of certificates and form of assumptions.
Relational abstraction replaces the differential equations in the system description by sound abstract discrete transitions, thus enabling application of discrete verification tools. The HybridSAL relational abstractor tool automatically computes such abstractions for linear hybrid systems. For nonlinear systems, both approaches require nonlinear constraint solvers. We improved an existing state-of-the-art symbolic nonlinear solver, but scalability continues to remain a challenge.
Related PublicationsRelated Posters Tool Download TBA