Safety Verification for Parameterized Hybrid Automata Networks

Date: Thursday, January 24, 2013
Speaker: Taylor Johnson
Venue: IST Austria

16:00 – 17:00

In this talk, I describe our work in automating thedeductive verification method of proving inductive invariants fornetworks of hybrid automata that are parameterized by the number ofinteracting automata. Our approach is inspired by the invisibleinvariants method for discrete systems. I present a small modeltheorem for hybrid automata networks, which allows us to reduce safetyverification of arbitrarily many interacting automata to verificationof a (usually small) finite number. The verification method isimplemented in a tool, Passel, which uses the Z3 satisfiability modulotheories (SMT) solver. I use the Small Aircraft Transportation System(SATS) landing protocol as an example, where aircraft coordinate toensure collisions do not occur while attempting to land at a runway.Lastly, I describe our current work to finish automating theverification process by synthesizing inductive invariants using SATSand Fischer’s mutual exclusion protocol as examples.

Posted in RiSE Seminar