曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
brat@email.arc.nasa.gov
ABSTRACT
In this paper we describe the design and implementation
of a static array-bound checker for a family of embedded
programs: the flight control software of recent Mars missions.
These codes are large (up to 280 KLOC), pointer
intensive, heavily multithreaded and written in an objectoriented
style, which makes their analysis very challenging.
We designed a tool called C Global Surveyor (CGS) that
can analyze the largest code in a couple of hours with a precision
of 80%. The scalability and precision of the analyzer
are achieved by using an incremental framework in which
a pointer analysis and a numerical analysis of array indices
mutually refine each other. CGS has been designed so that
it can distribute the analysis over several processors in a
cluster of machines. To the best of our knowledge this is
the first distributed implementation of static analysis algorithms.
Throughout the paper we will discuss the scalability
setbacks that we encountered during the construction of the
tool and their impact on the initial design decisions.
Categories and Subject Descriptors
F.3.2 [Logics and Meanings of Programs]: Semantics
of Programming Languages—Program Analysis
General Terms
Algorithms, Languages, Verification
Keywords
Abstract interpretation, program verification, pointer analysis,
array-bound checking, difference-bound matrices
1. INTRODUCTION
It is well-known that runtime errors plague the development
of large mission-critical software. In 1996, the explosion
of Ariane 501 shortly after launch was due to an overflow
in an arithmetic conversion. This failure cost over $500
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
PLDI’04, June 9–11, 2004, Washington, DC, USA.
Copyright 2004 ACM 1581138075/
04/0006 ...$5.00.
millions to the European space program. Classical verification
techniques based on development process, code reviewing
and testing were unable to detect that defect. This
overflow could have been detected by employing static analysis
techniques which can automatically inspect the text of a
program and check the safety of all operations. As a matter
of fact, the failure of Ariane 501 gave birth to a commercial
static analysis tool called PolySpace Ada Verifier [22]. This
tool can perform precise static analysis of large Ada programs
(over 1 MLOC) and find runtime errors. In previous
articles [5], we have reported our experience with C Verifier
(the C version of Ada Verifier) on real NASA software.
Unfortunately, we found that C Verifier does not scale as
well as its Ada counterpart. In short, we had to limit our
analysis to code pieces of 20 to 40 KLOC and we obtained
20% of warnings after 8 to 12 hours of analysis. This level
of performance was not enough to convince NASA software
developers to adopt the technology.
We analyzed the reasons for these limitations and we decided
to address them by prototyping our own static analysis
tool called C Global Surveyor (CGS). We believe that it is
extremely hard to build a static analyzer that works well
for any C programs. The precision of a static analysis tool
is measured in terms of the percentage of operations in the
program that can be decided as safe (or unsafe). Precision
is the main metric for judging the quality of a static analyzer.
Therefore, designing a static analyzer for any type of
C programs forces the tool implementer to make tradeoffs
that sacrifice scalability. We extensively experienced with
PolySpace C Verifier on a variety of NASA programs and we
observed that precision remained consistently around 80%.
However, there was a huge discrepancy between execution
times, from a couple of hours to days. Our driving philosophy
is that designing a tool for specific coding style and
software architecture allows us to make different tradeoffs
that optimize execution time for the software family we target.
Cousot et al. [3] used a similar approach to build a static
analyzer that is specialized for software developed by Airbus;
it can analyze 75,000 lines of C code without producing any
warnings. Our goal with CGS is not as ambitious. Whereas
the software analyzed in [3] is safety-critical, single-threaded
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(55)
