|go to week of Jul 27, 2014||27||28||29||30||31||1||2|
|go to week of Aug 3, 2014||3||4||5||6||7||8||9|
|go to week of Aug 10, 2014||10||11||12||13||14||15||16|
|go to week of Aug 17, 2014||17||18||19||20||21||22||23|
|go to week of Aug 24, 2014||24||25||26||27||28||29||30|
|go to week of Aug 31, 2014||31||1||2||3||4||5||6|
Computer-related defects in embedded and cyber-physical systems (CPS) are rampant, as exemplified by frequent product recalls in, for example, the automotive, healthcare, and consumer electronics industries. In this talk, I will first review some recent computer-related recalls by agencies like the National Highway Traffic Safety Agency (NHTSA), the Food and Drug Administration (FDA), and the Consumer Product Safety Commission (CPSC) to illustrate examples of cyber-physical defects and their root causes. I will then present our research contributions in developing formal verification techniques and software tools for CPS. One technique is for verifying distributed CPS where arbitrarily many agents (modeled as hybrid automata) participate in a common protocol, such as in air traffic control protocols, networked control systems, and swarm robotics. A subroutine in this method relies on computing reachable states for hybrid automata network instances, which is already challenging because of state-space explosion, so the technical focus of this talk is an abstraction method we call "anonymized reachability" that has been effective in reducing state-space explosion. Our implementation of this technique in a satisfiability modulo theories (SMT)-based software tool (called Passel) allows us to prove automatically, for example, that in one of NASA's conceptual air traffic control protocols, all aircraft maintain a safe separation, regardless of the number of aircraft. Finally, I will conclude with some CPS under development in our lab at UT Arlington that motivate extensions of existing parameterized verification frameworks, such as a modular networked continuous-culture bioreactor developed in conjunction with biologists at UT Southwestern and a distributed multilevel inverter for connecting renewables like photovoltaics to the smart grid. These prototype CPS are being used as case studies for evaluating our new formal verification techniques and tools.
Taylor T. Johnson is an Assistant Professor of Computer Science and Engineering at the University of Texas at Arlington. In 2013, he completed his PhD in Electrical and Computer Engineering (ECE) at the University of Illinois at Urbana-Champaign, where he worked in the Coordinated Science Laboratory with Prof. Sayan Mitra. He completed his MS in ECE at Illinois in 2010, earned a BSEE from Rice University in 2008, and was a visiting research assistant at the Air Force Research Laboratory's Space Vehicles Directorate at Kirtland Air Force Base in 2011. He worked in industry for Schlumberger at various times between 2005 and 2010, helping develop new downhole embedded control systems. Taylor's research focus is on developing algorithmic techniques and software tools to improve the reliability of cyber-physical systems. He has published over a dozen papers on these methods and their applications in areas like power and energy systems, aerospace, and robotics; two of them were recognized with best paper awards from the IEEE and IFIP. His research aims to develop reliable embedded and cyber-physical systems by advancing and applying techniques and tools from control theory, embedded systems, formal methods, and software engineering.