U.S. Used Key Tools to Examine Toyota Acceleration-Related Software
As part of the examination into the potential electronic causes of unintended acceleration in Toyota vehicles, the U.S. Department of Transportation has released the results of a 10-month investigation that included examination of more than 280,000 lines of code.
The investigation was conducted at the request of the National Highway Traffic Safety Administration (NHTSA) of the U.S. Department of Transportation, in collaboration with the National Air and Space Administration’s (NASA) Engineering and Safety Center (NESC). The object was to see if the cause for unintended acceleration events could be found in software.
The tools used in the testing included: CodeSonar from GrammaTech, Prevent from Coverity, and Spin, a model checker from an open-source project.
GrammaTech, founded by Professors Tim Teitelbaum of Cornell University and Tom Reps of the University of Wisconsin, makes status analysis tools; its staff includes 13 Ph.D.-level experts.
GrammaTech offers static analysis and program transformation tools, including the flagship CodeSurfer/CodeSonar static-analysis platform for analyzing source code. In addition, the company has developed versions of CodeSurfer and CodeSonar for analyzing binaries, as in stripped executables or machine code.
The products of Coverity, focused on software integrity, were developed in the Computer Systems Laboratory at Stanford University in Palo Alto, Calif., from 1999 through 2002. First called MC Checker, Prevent was used to find defects in open-source projects such as Linux and FreeBSD. The product was commercialized within Coverity. Today, Coverity’s product can scale to tens of millions of lines of code, so it is used by large companies worldwide.
Coverity Static Analysis, Coverity Dynamic Analysis, Coverity Architecture Analysis, and Coverity Build Analysis help software companies deliver high-integrity software with emphasis on performance, reliability, and security.
The Spin project’s Uno tool, dating to 2001, checks for the three most common types of software defects (use of uninitialized variable, nil-pointer references, and out-of-bounds array indexing), and it allows for the checking of a broad range of user-defined properties. These properties can be specified, for instance, for checking lock-order disciplines, compliance with user-defined interrupt masking rules, and rules stipulating that all memory allocated must be freed.
The extensive government report found no direct cause for unintended acceleration in the vehicles, although it could not be decisively ruled out within the scope of the study. Several candidate theories were disproven.
Other findings: The Toyota software development process uses a “proprietary-developed coding standard;” there are no methods for capturing pre-event software state and performance following an unintended acceleration (UA) event either on the vehicle or as a diagnostic tool; and from extensive software testing and analysis performance on the TMC 2005 Camry L4 source code using static analysis, logic model testing, recursion testing, and worst-case execution timing, “software defects that unilaterally cause a UA were not found,” the report stated.
The full report can be found at: http://www.nhtsa.gov/staticfiles/nvs/pdf/NASA-UA_report.pdf
For more information, go to:
Feb2011, Software Magazine