Progress on Powertrain Verification Challenge with C2E2

TitleProgress on Powertrain Verification Challenge with C2E2
Publication TypeConference Paper
Year of Publication2015
AuthorsFan C, Duggirala PSridhar, Mitra S, Viswanathan M
EditorFrehse G, Althoff M
Conference NameInternational Workshop on Applied Verification for Continuous and Hybrid Systems, (ARCH)
Conference LocationSeattle, 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.