Statistical Verification of the Toyota Powertrain Control Verification Benchmark poster
The powertrain control problem is one of regulating the air-to-fuel ratio in an automotive engine. A series of models of such controllers, with increasing levels of sophistication and fidelity to real-world designs, have been recently proposed by Toyota researchers as challenge problems for today’s verification technologies. In this work we present our results in verifying the most complicated of the models proposed in Toyota (Model 1) that has features like delayed differential and difference equations, look-up tables, in addition to highly non-linear continuous dynamics for the state variables.
Our approach is to simulate the C++ code generated automatically from the Simulink design of the system for randomly chosen values for the parameters of engine speed and signal profile. We then check if the sample drawn provides statistical evidence of the satisfaction of the key properties of the system, using hypothesis testing. Our analysis confirms that for at least 98% of the choices for values of the initial parameters, the key properties of the system hold. Since our analysis is statistical, there is a probability that our analysis is incorrect; this error is bounded by 0.001 for our experiments reported here.
These are the first mathematical guarantees of correctness obtained for Model 1 presented by Toyota. Previously, the falsification tool S-Taliro was used to search for possible counterexamples. Also, the significantly simpler Model 3 (with polynomial dynamics) was verified with the tool C2E2
Submitted by Geir Dullerud
on
The powertrain control problem is one of regulating the air-to-fuel ratio in an automotive engine. A series of models of such controllers, with increasing levels of sophistication and fidelity to real-world designs, have been recently proposed by Toyota researchers as challenge problems for today’s verification technologies. In this work we present our results in verifying the most complicated of the models proposed in Toyota (Model 1) that has features like delayed differential and difference equations, look-up tables, in addition to highly non-linear continuous dynamics for the state variables.
Our approach is to simulate the C++ code generated automatically from the Simulink design of the system for randomly chosen values for the parameters of engine speed and signal profile. We then check if the sample drawn provides statistical evidence of the satisfaction of the key properties of the system, using hypothesis testing. Our analysis confirms that for at least 98% of the choices for values of the initial parameters, the key properties of the system hold. Since our analysis is statistical, there is a probability that our analysis is incorrect; this error is bounded by 0.001 for our experiments reported here.
These are the first mathematical guarantees of correctness obtained for Model 1 presented by Toyota. Previously, the falsification tool S-Taliro was used to search for possible counterexamples. Also, the significantly simpler Model 3 (with polynomial dynamics) was verified with the tool C2E2