IKOS, a high-performance static code analysis platform, has met the FY’12 APG milestone in AFCS (formerly known as VVFCS) in the SSAT project of the Aviation Safety program. The milestone set to achieve less than 5% false positives for the static analysis of flight critical code in C and C++. IKOS achieved close to 2% false positives on a suite of flight control systems written in C and C++.
This achievement represents a significant improvement over available commercial static analyzers both in terms of precision and analyze time (from hours, if not days, for the most precise commercial analyzers to seconds or minutes for IKOS). IKOS is also demonstrating a wider applicability than research tools; it is applicable to general C programs, even though it is particularly performant for embedded code, or code auto-generated from MATLAB/Simulink.
IKOS was presented at ARC on March 27, 2012 to the ARMD upper management, Dr. Jaiwon Shin and Tom Irvine, as well as John Tracey (CTO for The Boeing Company).
BACKGROUND: IKOS is the new generation of static analysis tools designed by the RSE group. It is drawing on lessons learned from designing the C Global Surveyor static analyzer, which had achieved significant improvement in analysis time on the flight code of Mars rover missions. IKOS is built on top of the LLVM programmable compiler front-end. It works on virtually any C and C++ program, especially when those can be compiled using gcc.
NASA PROGRAM FUNDING: IKOS is funded by the Aviation Safety program in ARMD through the AFCS element of the SSAT project.
TEAM: ARC TI: Arnaud Venet (CMU), Sarah Thompson (SGT Inc.), and Guillaume Brat (CMU)
Contact: Arnaud Venet