Communications - April 2009

try regards as too costly (such as formal specification and static analysis of code) can actually reduce overall cost. ²

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.

Acknowledgments

The key ideas in this article come from a National Academies study that I

22

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 the Academies.

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 particular topics.

A version of this article with a fuller list of references is available at http:// sdg.csail.mit.edu/publications.html.

References

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. 2005).

22. amey, P. correctness by construction: better can also be cheaper. Cross Talk: the journal of Defense software engineering (mar. 2002); www.praxis-his. com/pdfs/c_by_c_better_cheaper.pdf.

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; googleresearch.blogspot.com/2006/06/extra-extra- read-all-about-it-nearly.html.

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/ documents/ashP_chapter.pdf.

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 (springer-Verlag), 1997.

9. fDa. Ensuring the safety of marketed medical devices: CDRH’s medical device post-market safety program, 2006.

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/ shuttle/missions/51-l/docs/rogers-commission/ appendix-f.txt.

11. gallaher, m. and kropp, b. Economic Impacts of Inadequate Infrastructure for Software Testing, national institute of standards and technology, 2002.

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. spectrum.ieee.org/nov04/4015.

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., 2001.

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. 1996).

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, 2001).

18. hatton, l. and safer c. Developing Software in High-Integrity and Safety-Critical Systems. mcgraw-hill, 1995.

19. holzmann, g. the power of ten: rules for developing safety critical code. IEEE Computer 39, 6, (june 2006).

20. iaea. Investigation of an Accidental Exposure of Radiotherapy Patients in Panama: Report of a Team of Experts. (Vienna, austria, may 26–june 1, 2001); www-pub.iaea.org/mtcD/publications/PDf/ Pub1114_scr.pdf.

21. jackson, D. Dependable software by design. Scientific American (june 2006); www.sciam.com/ article.cfm?id=dependable-software-by-de&collD= 1.

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. php?isbn=0309103940.

23. jackson, m. Problem frames: analysing and structuring software Development Problems. addison-Wesley, 2001.

24. gross, g. e-voting vendor: Programming errors caused dropped votes. Network World (aug. 22, 2008); www.net workworld.com/news/2008/082208- e-voting-vendor-programming-errors-caused.html.

25. krebs, b. cyber incident blamed for nuclear power plant shutdown. Washington Post (june 5, 2008); www.washingtonpost.com/wp-dyn/content/ article/2008/06/05/ ar2008060501958_pf.html.

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/ publications/incidents/Docs/comandrep/Warsaw/ warsaw-report.html.

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 Press, 1999.

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. 1997).

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. pqarchiver.com/baltsun/access/1502776681.html?d ids=1502776681:1502776681&fmt=abs&fmts=a bs:ft&type=current&date=jun+30%2c+2008&aut hor=jonathan+D.+rockoff&pub=the+sun&desc=fl aWs+in+meDical+coDing+can+kill.

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/ security/news/2003/12/61637.

Daniel Jackson ( dnj@mit.edu) 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, cambridge, ma.