NHTSA-NASA Study of Unintended Acceleration in Toyota Vehicles

NHTSA-NASA Study of Unintended Acceleration in Toyota Vehicles @ http://www.nhtsa.gov/UA

The report may be found @ http://www.nhtsa.gov/staticfiles/nvs/pdf/NHTSA-UA_report.pdf

NASA team applied static source-code analysis, formal logic model checking, and algorithm analysis through simulation.

The report states "The team's experience is that there is no single analysis technique today that can reliably intercept all vulnerabilities, but that it is strongly recommended to deploy a range of different leading tools."

For code analysis, the team used Coverity, CodeSonar, and Bell Labs' Uno to identify common coding defects and suspicious coding patterns. The team also used CodeSonar to compare Toyota's code against a Jet Propulsion Lab coding standards (1,2,3).

For model checking, the team used open-source Spin and Swarm. To use a formal model checker, one first has to write formal models. The team built models only for those software modules it believed could be culprits; the formal analysis depended on human judgment.

The algorithm analysis began with building models in Matlab. This process started with reading Toyota documentation and talking with Toyota engineers, and then progressed to analyzing the source code and finally testing the models against actual Camrys. Once the NASA team was satisfied with the models, they explored failure scenarios in Simulink and checked delays with AbsInt aiT.

Some conclusions suggest themselves. First, there are no silver bullets: effective debug means using everything you've got.

Second, even when it's grounded in exhaustive and formal techniques, an evaluation is circumscribed by the evaluators' beliefs about the possible behavior of the system.

Third, there is no certainty. Despite Toyota's great care in developing their code, NASA's analysis found significant errors, including serious underestimates of delays in the multiprocessing system.

But the investigation could not link those errors to any proposed mechanism for unintended acceleration. NASA Executive Summary stated "Because proof that the ETCS-i caused the reported UAs [unintended accelerations] was not found does not mean it could not occur."