We used an improved version of C2E2 to verify a challenging automotive benchmark system. This model comes from a suite of benchmarks from our friends at Toyota that were posed as a challenge problem for the hybrid systems community, and to our knowledge, we are reporting its first verification. For this work, we implemented the algorithm reported in this tech report in C2E2, to automatically compute local discrepancy (rate of convergence or divergence of trajectories) of the model. We verify the key requirements of the model, specified in signal temporal logic (STL), for a set of driver behaviors. The paper that describes the case study and our approach can be obtained here. A progress report, which includes technical details, implementation challenges, and outlines the next set of goals can be obtained here.
For repeatability of our results, we have created a virtual machine that contains the build of C2E2 for powertrain verification. The virtual machine can be downloaded here. This VM image was created using VirtualBox and hence we recommend using the same for reproducing the results. The instructions for running the powertrain verification benchmark are provided in the virtual machine.