Monday, April 18, 2016
Speaker: Stanley Bak
Venue: IST Austria
Room: Mondi 2.
Hybrid automata formally model the evolution of a continuous, time-evolving system that undergoes discrete changes, such as interactions with an embedded controller. Examining which states a hybrid automaton can reach, in order to verify formal properties, is challenging. The research community, however, is quite innovative, and continues to propose a large number of promising approaches.
In order to verify high-level properties of hybrid automata, multiple techniques or iterations or a technique may need to be used. In particular, the recent tools Hyst and Hypy enable this type of heterogeneous and multi-iteration analysis. Hyst is used to encode individual model transformations (tactics), whereas Hypy can guide the use of these techniques (strategies) by running reachability tools and interpreting the tools’ results. Finally, verifying general cyber-physical systems inevitably involves the software domain, which has its own domain-specific set of analysis techniques. Those reasoning approaches also need to be integrated in order to perform high-level formal reasoning.
Stanley Bak is a computer science researcher in the field of formal verification of cyber-physical systems using hybrid automata models. His recent research aims to develop tools and techniques for automatic and scalable formal reasoning of complex system models.
Stanley Bak received a Bachelor’s degree in Computer Science from Rensselaer Polytechnic Institute (RPI) in 2007 (summa cum laude), and a Master’s degree in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2009. He completed his PhD from the Department of Computer Science at UIUC in 2013. He received the Founders Award of Excellence for his undergraduate research at RPI in 2004, the Debra and Ira Cohen Graduate Fellowship from UIUC twice, in 2008 and 2009, and was awarded the Science, Mathematics and Research for Transformation (SMART) Scholarship from 2009 to 2013. He is currently a research computer scientist at the United States Air Force Research Laboratory (AFRL), working in the Verification of Autonomous Systems Branch and the Aerospace Systems Directorate.