@InProceedings{FDMV:ARCH2015,
  author    = {Chuchu Fan and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan},
  title     = {Progress on Powertrain Verification Challenge with C2E2},
  booktitle = {Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015)},
  year      = {2015},
  abstract  = {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 [FanM:2015] 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.},
  codeurl   = {https://publish.illinois.edu/c2e2-tool/},
  keywords  = {Automotive systems},
  notes     = {<b>Robert Bosch sponsored best verification result award.</b>},
  owner     = {mitras},
  pdfurl    = {research/2015/arch2015.pdf},
  timestamp = {2015.05.04},
}