Verifying hybrid system designs against requirements is a difficult task, and there is a lack of suitable open benchmark models to assess, evaluate, and compare tools and techniques. Benchmark models can be valuable for the hybrid systems research community, as they can communicate the nature and complexity of the problems facing industrial practitioners. We present a series of benchmark verification problems from the automotive control domain; the problems are intended to challenge the research community while maintaining a manageable scale. We present three hybrid automaton models of a fuel control system, implemented in the Simulink ® modeling environment, along with representative requirements in signal temporal logic (STL). We conclude with a discussion of challenges for the research community.
Jim received his Ph.D. in Electrical and Computer Engineering from Carnegie Mellon University in 2005 and was a postdoctoral researcher at CMU from 2007 to 2008. He went on to found and lead Fixed-Point Consulting, serving clients in the defense, aerospace, and automotive industries. Since 2012 he has been with the Model-Based Development group at the Toyota Technical Center in Los Angeles, serving as a Principal Engineer. His work at Toyota focuses on advanced research into verification techniques for embedded software for powertrain control systems. Jim’s research interests involve verification techniques for embedded control system designs and analysis of hybrid dynamical systems.
yano [atsymbol] cs.cmu.edu