|Title||Progress on Powertrain Verification Challenge with C2E2|
|Publication Type||Conference Paper|
|Year of Publication||2015|
|Authors||Fan C, Duggirala PSridhar, Mitra S, Viswanathan M|
|Editor||Frehse G, Althoff M|
|Conference Name||International Workshop on Applied Verification for Continuous and Hybrid Systems, (ARCH)|
|Conference Location||Seattle, WA, USA|
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 for computing local discrepancy (rate of convergence or divergence of trajectories) reported in the hybrid system verification tool C2E2. 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.