try regards as too costly (such as formal specification and static analysis of
code) can actually reduce overall cost. 2
Similarly, even though the augmentation of testing with more ambitious
analysis tools will require greater expertise than is available to many teams
today, this avenue does not necessarily
increase the cost either. When low levels of confidence suffice, testing may be
the most cost-effective way to establish
dependability. As the required level of
confidence rises, though, testing soon
becomes prohibitively expensive, and
the use of more sophisticated methods
is likely to be more economical. Invariants may be harder to write than test
cases, but a single invariant defines an
infinite number of test cases, so a decision to write one (and use a tool that
checks all the cases it defines) will pay
off very soon.
Efforts to make software more dependable or secure are inherently conservative and therefore risk retarding
progress, and many practitioners understandably see certification schemes and
standards as millstones around their
necks. But because a direct approach
based on dependability cases gives developers an incentive to use whatever
development methods and tools are
most economic and effective, the approach therefore rewards innovation.
The key ideas in this article come from
a National Academies study that I
chaired. I am very grateful to the members of my committee—Joshua Bloch,
Michael DeWalt, Reed Gardner, Peter
Lee, Steven Lipner, Charles Perrow,
Jon Pincus, John Rushby, Lui Sha, Martyn Thomas, Scott Wallsten, and David
Woods; to our study director Lynnette
Millett; to Jon Eisenberg, director of
the Academies’ Computer Science
and Telecommunications Board; and
to our sponsors, especially Helen Gill,
who was instrumental in making the
case for the study. John Rushby and
Martyn Thomas deserve recognition
for having been long and eloquent advocates of the direct approach. Many
of the opinions expressed in this article, however, are my own and have not
been approved by the committee or by
Thanks too to Butler Lampson,
Shari Lawrence Pfleeger, and Derek
Rayside, who gave extensive and helpful suggestions on an initial draft of the
article; to the anonymous reviewers;
and to Hari Balakrishnan, Bill Maisel
and Andrew Myers who gave valuable
feedback and shared their expertise on
A version of this article with a fuller
list of references is available at http://
1. aiken, a. and xie, y. context- and path-sensitive
memory leak detection. Proceedings of the 5th
Joint Meeting of the European Software Engineering
Conference and the ACM SIGSOFT Symposium
on the Foundations of Software Engineering (sept.
22. amey, P. correctness by construction: better can
also be cheaper. Cross Talk: the journal of Defense
software engineering (mar. 2002); www.praxis-his.
3. ball, t. and rajamani, s. the slam project:
Debugging system software via static analysis.
in Proceedings of the 29th ACM Symposium on
Principles of Programming Languages (Portland,
oregon, jan. 16–18), 2002.
4. bloch, j. extra, extra—read all about it: nearly
all binary searches and mergesorts are broken;
5. cone, e. the ugly history of tool development at the
faa. Baseline Magazine 4, 9 (apr. 8, 2002).
6. cook, r. and o’connor, m. thinking about accidents
and systems. in Medication Safety: A Guide to
Health Care Facilities, h.r. manasse and k.k.
thompson, eds. american society of health-system
Pharmacists, Washington, Dc, 2005; www.ctlab.org/
7. cousot, P. Proving the absence of run-time errors
in safety-critical avionics code. in Proceedings of
the Seventh ACM & IEEE International Conference
on Embedded Software. (salzburg, austria, sept.
30–oct. 3), acm Press, new york, 2007.
8. Dijkstra, e. W. the tide, not the waves. in Beyond
Calculation: The Next Fifty Years of Computing,
Denning, P. and metcalfe, r., eds. copernicus
9. fDa. Ensuring the safety of marketed medical
devices: CDRH’s medical device post-market safety
10. feynman, r.P. appendix f: Personal observations
on the reliability of the shuttle. in Report of the
Presidential Commission on the Space Shuttle
Challenger Accident, 1986; science.ksc.nasa.gov/
11. gallaher, m. and kropp, b. Economic Impacts of
Inadequate Infrastructure for Software Testing,
national institute of standards and technology,
12. gao. Medical Devices: Early Warning of Problems Is
Hampered by Severe Under-reporting. Publication
PemD- 87-1, u.s. government Printing office, 1986.
13. geppert, l. lost radio contact leaves pilots on their
own. IEEE Spectrum 41, 11 (nov. 2004); www.
14. german, a. and mooney, g. air vehicle software static
code analysis—lessons learnt. in Proceedings of the
Ninth Safety-Critical Systems Symposium, f. redmill
and t. anderson, eds. springer-Verlag, bristol, u.k.,
15. griswold, W. coping with crosscutting software
changes using information transparency. in
Reflection 2001: The Third International Conference
on Metalevel Architectures and Separation of
Crosscutting Concerns (kyoto, sept. 25–28, 2001).
16. hall, a. using formal methods to develop an atc
information system. IEEE Software 13, 2 (mar.
17. hammond, j., rawlings, r., and hall, a. Will it work?
in Proceedings of the 5th International Symposium
on Requirements Engineering (toronto, aug. 27–31,
18. hatton, l. and safer c. Developing Software in High-Integrity and Safety-Critical Systems. mcgraw-hill,
19. holzmann, g. the power of ten: rules for developing
safety critical code. IEEE Computer 39, 6, (june
20. iaea. Investigation of an Accidental Exposure
of Radiotherapy Patients in Panama: Report of a
Team of Experts. (Vienna, austria, may 26–june 1,
21. jackson, D. Dependable software by design.
Scientific American (june 2006); www.sciam.com/
22. jackson, D., thomas, m., and millett, l., eds.
Software For Dependable Systems: Sufficient
Evidence? national research council. national
academies Press, 2007; books.nap.edu/openbook.
23. jackson, m. Problem frames: analysing and
structuring software Development Problems.
24. gross, g. e-voting vendor: Programming errors
caused dropped votes. Network World (aug. 22,
2008); www.net workworld.com/news/2008/082208-
25. krebs, b. cyber incident blamed for nuclear power
plant shutdown. Washington Post (june 5, 2008);
26. ladkin, P., transcriber. Transcription of Report on the
Accident of Airbus A320-211 Aircraft in Warsaw on
Sept. 14, 1993. main commission aircraft accident
investigation Warsaw; www.rvs.uni-bielefeld.de/
27. liskov, b. a history of clu. ACM SIGPLAN Notices
28, 3 (mar. 1993).
28. littlewood, b. and Wright, D. some conservative
stopping rules for the operational testing of safety-critical software. IEEE Transactions on Software
Engineering 23, 11 (nov. 1997).
29. mackenzie, D. Mechanizing Proof: Computing, Risk,
and Trust. mit Press, 2001.
30. maisel, W., sweeney, m., stevenson, W., ellison, k.,
and epstein, l. recalls and safety alerts involving
pacemakers and implantable cardioverter-defibrillator generators. Journal of the American
Medical Association 286, 7 (aug. 15, 2001).
31. ministry of Defence. Defence Standard 00-42:
Reliability And Maintainability Assurance Guides,
Part 2: Software, 1997.
32. Parnas, D. and madey, j. functional documentation
for computer systems. Science of Computer
Programming 25, 1 (1995).
33. Perrow, c. Normal Accidents, Princeton university
34. Perrow, c. The Next Catastrophe: Reducing our
Vulnerabilities to Natural, Industrial, and Terrorist
Disasters. Princeton university Press, 2004.
35. Pfleeger, s. and hatton, l. investigating the
influence of formal methods. Computer 30, 2 (feb.
36. rockoff, j. flaws in medical coding can kill: spread
of computers creates new dangers, fDa officials
warn. Baltimore Sun (june 30, 2008); http://pqasb.
37. salvadori, m. Why Buildings Stand Up: The Strength
of Architecture. norton, 1980. see also levy, m.
and salvadori, m. Why Buildings Fall Down: How
Structures Fail. norton, 1992.
38. slabodkin, g. navy: calibration flaw crashed
yorktown lan. Government Computing News (nov.
9, 1998); www.gcn.com/print/17_30/33914-1.html.
39. Zetter, k. e-voting undermined by sloppiness. Wired
(December 17, 2003); www.wired.com/politics/
Daniel Jackson ( firstname.lastname@example.org) is a professor of
computer science at the massachusetts institute
of technology and a principal investigator at mit’s
computer science and artificial intelligence lab,
© 2009 acm 0001-0782/09/0400 $5.00
88 communicAtionS of the Acm | APriL 2009 | voL. 52 | no. 4