Corina Mitrohin:
Hybrid System Abstraction via Dwelling Times

Abstract: Reachability analysis for hybrid systems is known as being a hard task and it has been motivated by safety verification. More recent work in region stability verification produced a proof rule whose implementation reduces the verification task to reachability analysis, with the bottleneck of applying this analysis to a hybrid system containing a duplicated number of continuous variables. As consequence, it can be the case that a system with only three continuous variables can not be proven as being stable with respect to a certain region. In this talk we present the dwelling time bound abstraction. Our method replaces continuous variables which do not occur explicitly in the property to be proven through information about the time spent in one location. We call this information dwelling time bound. We applied this abstraction technique for region stability verification and succeeded in proving stability for hybrid systems, for which such properties could not be shown up to now.

Bio:
Corina Mitrohin received a B.Sc. degree in computer science from the University of Iasi, Romania, in 2000, and an M.Sc. degree in applied computer science from University of Freiburg, Germany, in 2007. After receiving her M.Sc., she joined the research group headed by Prof. Dr. Andreas Podelski at the University of Freiburg and is now a PhD student. Mitrohin's interests include formal verification techniques, model checking, hybrid systems verification, stability properties, abstraction techniques therefore. In her B.Sc. thesis she proposed a code with synchronization words that can be used for data compression. In her M.Sc. thesis she developed a method for automatic consistency checking for requirements, and succeeded applying this method to a real-life example. Corina’s current work is focused on decomposition and abstraction techniques for model checking hybrid systems.

Appointments: dcm@cs.cmu.edu

Maintainer [ Home > Seminar ]
`Last modified: Tues Sep 30 11:09:10 EDT 2008