Progress on Powertrain Verification Challenge with C2E2

In this paper, we present the progress we have made in verifying the benchmark powertrain control systems introduced in the last ARCH workshop. We implemented the algorithm reported in [8] in the hybrid system verification tool C2E2 for automatically computing local discrepancy (rate of convergence or divergence of trajectories). We created Stateflow translations of the original models to aid the processing using C2E2 tool. We also had to encode the different driver behaviors in the form of state machines. With these customizations, we have been successful in verifying one of the easier (but still challenging) benchmarks from the powertrain suite. In this paper, we present some of the engineering challenges and describe the artifacts we created in the process. 1 The Powertrain Benchmarks The benchmark suite of powertrain control systems were published in [10,9] as challenge problems for hybrid system verification. The suite has a set of SimulinkTM models with increasing levels of sophistication and fidelity. At a high-level, all the models take inputs from a driver (throttle angle) and the environment (sensor failures), and define the dynamics of the engine. The key controlled quantity is the air to fuel ratio which in turn influences the emissions, the fuel efficiency, and torque generated. The first model (model 1) is the most complex. It has look-up tables, delayed differential equations, and switches. Models 2 and 3 are simpler but still complicated enough for most hybrid verifcation tools. Model 3 is a hybrid automaton with polynomial differential equations and continuously computed control inputs, and Model 2 is similar but with nonlinear differential equations and both continuous and discretely sampled variables. The requirements for the system are stated in signal temporal logic (STL). A typical property, for example, 3t(x ∈ [xeq − , xeq + ]), states that after t units of time, the continuous variable x is within the range xeq ± . ? The results reported here have beed submitted for peer-review, however, this paper presents several technical details and artifacts for the first time. We thank Jim Kapinski, Jyotirmoy Deshmukh, and Xiaoqing Jin of Toyota for several useful discussions on the powertrain models. This research is funded by research grants from the National Science Foundation (grant: CAR 1054247 and NSF CSR 1016791) and the Air Force Office of Scientific Research (AFOSR YIP FA9550-12-1-0336).