SOFTWARE FOR DEPENDABLE SYSTEMS
SUFFICIENT EVIDENCE?
Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors
THE NATIONAL ACADEMIES PRESS
Washington, D.C.
www.nap.edu
THE NATIONAL ACADEMIES PRESS
500 Fifth Street, N.W. Washington, DC 20001
NOTICE: The project that is the subject of this report was approved by the Governing Board of the National Research Council, whose members are drawn from the councils of the National Academy of Sciences, the National Academy of Engineering, and the Institute of Medicine. The members of the committee responsible for the report were chosen for their special competences and with regard for appropriate balance.
Support for this project was provided by the National Science Foundation and the National Security Agency under sponsor award number CCR-0236725; the Office of Naval Research under sponsor award number N00014-03-1-0915; and the National Science Foundation, the National Security Agency, and the Federal Aviation Administration under sponsor award number CNS-0342801. Any opinions, findings, or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the agencies and organizations that provided support for the project.
International Standard Book Number-13: 978-0-309-10394-7
International Standard Book Number-10: 0-309-10394-0
Additional copies of this report are available from
The National Academies Press
500 Fifth Street, N.W., Lockbox 285 Washington, DC 20055 (800) 624-6242 (202) 334-3313 (in the Washington metropolitan area) http://www.nap.edu
Copyright 2007 by the National Academy of Sciences. All rights reserved.
Printed in the United States of America
THE NATIONAL ACADEMIES
Advisers to the Nation on Science, Engineering, and Medicine
The National Academy of Sciences is a private, nonprofit, self-perpetuating society of distinguished scholars engaged in scientific and engineering research, dedicated to the furtherance of science and technology and to their use for the general welfare. Upon the authority of the charter granted to it by the Congress in 1863, the Academy has a mandate that requires it to advise the federal government on scientific and technical matters. Dr. Ralph J. Cicerone is president of the National Academy of Sciences.
The National Academy of Engineering was established in 1964, under the charter of the National Academy of Sciences, as a parallel organization of outstanding engineers. It is autonomous in its administration and in the selection of its members, sharing with the National Academy of Sciences the responsibility for advising the federal government. The National Academy of Engineering also sponsors engineering programs aimed at meeting national needs, encourages education and research, and recognizes the superior achievements of engineers. Dr. Charles M. Vest is president of the National Academy of Engineering.
The Institute of Medicine was established in 1970 by the National Academy of Sciences to secure the services of eminent members of appropriate professions in the examination of policy matters pertaining to the health of the public. The Institute acts under the responsibility given to the National Academy of Sciences by its congressional charter to be an adviser to the federal government and, upon its own initiative, to identify issues of medical care, research, and education. Dr. Harvey V. Fineberg is president of the Institute of Medicine.
The National Research Council was organized by the National Academy of Sciences in 1916 to associate the broad community of science and technology with the Academy’s purposes of furthering knowledge and advising the federal government. Functioning in accordance with general policies determined by the Academy, the Council has become the principal operating agency of both the National Academy of Sciences and the National Academy of Engineering in providing services to the government, the public, and the scientific and engineering communities. The Council is administered jointly by both Academies and the Institute of Medicine. Dr. Ralph J. Cicerone and Dr. Charles M. Vest are chair and vice chair, respectively, of the National Research Council.
COMMITTEE ON CERTIFIABLY DEPENDABLE SOFTWARE SYSTEMS
DANIEL JACKSON,
Massachusetts Institute of Technology,
Chair
JOSHUA BLOCH,
Google Inc.
MICHAEL DeWALT,
Certification Systems, Inc.
REED GARDNER,
University of Utah School of Medicine
PETER LEE,
Carnegie Mellon University
STEVEN B. LIPNER,
Microsoft Trustworthy Computing Group
CHARLES PERROW,
Yale University
JON PINCUS,
Microsoft Research
JOHN RUSHBY,
SRI International
LUI SHA,
University of Illinois at Urbana-Champaign
MARTYN THOMAS,
Martyn Thomas Associates
SCOTT WALLSTEN,
Progress and Freedom Foundation
DAVID WOODS,
Ohio State University
Staff
LYNETTE I. MILLETT, Study Director and Senior Program Officer
DAVID PADGHAM, Associate Program Officer
GLORIA WESTBROOK, Senior Program Assistant (through November 2006)
PHIL HILLIARD, Research Associate (through May 2004)
PENELOPE SMITH, Senior Program Assistant (February 2004-July 2004)
COMPUTER SCIENCE AND TELECOMMUNICATIONS BOARD
JOSEPH F. TRAUB,
Columbia University,
Chair
ERIC BENHAMOU,
Benhamou Global Ventures, LLC
FREDERICK R. CHANG,
University of Texas, Austin
WILLIAM DALLY,
Stanford University
MARK E. DEAN,
IBM Almaden Research Center
DEBORAH ESTRIN,
University of California, Los Angeles
JOAN FEIGENBAUM,
Yale University
KEVIN KAHN,
Intel Corporation
JAMES KAJIYA,
Microsoft Corporation
MICHAEL KATZ,
University of California, Berkeley
RANDY H. KATZ,
University of California, Berkeley
SARA KIESLER,
Carnegie Mellon University
TERESA H. MENG,
Stanford University
PRABHAKAR RAGHAVAN,
Yahoo! Research
FRED B. SCHNEIDER,
Cornell University
ALFRED Z. SPECTOR, Independent Consultant,
Pelham, New York
WILLIAM STEAD,
Vanderbilt University
ANDREW J. VITERBI,
Viterbi Group, LLC
PETER WEINBERGER,
Google Inc.
JEANNETTE M. WING,
Carnegie Mellon University
Staff
JON EISENBERG, Director
KRISTEN BATCH, Associate Program Officer
RADHIKA CHARI, Administrative Coordinator
RENEE HAWKINS, Financial Associate
MARGARET MARSH HUYNH, Senior Program Assistant
HERBERT S. LIN, Senior Scientist
LYNETTE I. MILLETT, Senior Program Officer
DAVID PADGHAM, Associate Program Officer
JANICE M. SABUDA, Senior Program Assistant
TED SCHMITT, Consultant
BRANDYE WILLIAMS, Program Assistant
JOAN D. WINSTON, Program Officer
For more information on CSTB, see its Web site at <http://www.cstb.org>, write to CSTB, National Research Council, 500 Fifth Street, N.W., Washington, DC 20001, call (202) 334-2605, or e-mail CSTB at cstb@nas.edu.
Preface
Critical systems are often subject to certification: a formal assurance that the system has met relevant technical standards designed to ensure it will not unduly endanger the public and can be depended upon to deliver its intended service safely and securely. Today, certification1 of the dependability of a software-based system usually relies more on assessments of the process used to develop the system than on the properties of the system itself. While these assessments can be useful, few would dispute that direct observation of the artifact ought to provide a stronger kind of assurance than the credentials of its production method. Yet the complexity of software systems, as well as the discontinuous way they behave, renders them extremely difficult to analyze unless great care has been taken with their structure and maintenance.
To further understand these and related issues, the High Confidence Software and Systems (HCSS) Coordinating Group (CG) of the National Science and Technology Council’s Networking and Information Technology Research and Development (NITRD) Subcommittee initiated discussions with the Computer Science and Telecommunications Board (CSTB) of the National Research Council (NRC). These discussions resulted in a study to assess the current state of certification in dependable systems with the goal of recommending areas for improvement. Funding
for the project was obtained from the following HCSS CG agencies: the National Science Foundation, the National Security Agency, the Office of Naval Research, and the Federal Aviation Administration.
A committee was formed consisting of 13 experts from industry and academia specializing in diverse aspects of systems dependability including software engineering, software testing and evaluation, software dependability, embedded systems, human-computer interaction, systems engineering, systems architecture, accident theory, standards setting, avionics, medicine, economics, security, and regulatory policy (see Appendix A for committee and staff biographies).
To accomplish its mission, the committee divided the study into two phases: a framing phase and an assessment phase. The framing phase culminated in a public workshop in April 2004, attended by members of industry, government, and academia. The workshop was organized as a series of panel discussions on a variety of topics and was summarized by the committee in a subsequent report.2
In the assessment phase of the study, the committee held a series of meetings over a 2-year period. Each meeting comprised a day of open sessions in which the committee heard opinions and evidence from a variety of experts, and 1 or 2 days of closed sessions in which the committee analyzed the information presented to it and worked to develop a view on the state of software dependability and recommendations for the future. The chair of the committee also conducted a handful of telephone interviews with experts to supplement the material covered during the committee’s meetings.
This report adopts a broad perspective on the question of how software might be made dependable in a cost-effective manner rather than focusing narrowly on the question of software certification per se. By design, this diverse committee represented a range of views on issues, and with this wider perspective, the committee found itself confronting the perennial dilemmas of software engineering, discussing in a current context many of the same issues that have been debated since a seminal 1968 NATO conference.3 In discussions and through the process of writing the report, a number of these issues were explored, including the likelihood of catastrophes caused by software; whether formal methods will scale to large systems; and the extent to which a manufacturer’s disclaim-
2 |
National Research Council, 2004, Summary of a Workshop on Software Certification and Dependability, The National Academies Press, Washington, D.C. Available online at <http://books.nap.edu/catalog/11133.html>. |
3 |
See P. Naur and B. Randell, eds., 1969, “Software engineering: Report on a conference sponsored by the NATO Science Committee,” Garmisch, Germany, October 7-11, 1968, NATO Scientific Affairs Division, Brussels, Belgium. Available online at <http://homepages.cs.ncl.ac.uk/brian.randell/NATO/>. |
ing of liability should be seen as undermining any dependability claims it makes. Although this study does not attempt to resolve these longstanding issues, the committee believes that the recommendations and approach set forth in this report can be used in the short term to improve the dependability of systems and in the longer term to lay the foundation for new and more powerful software development methods.
The committee thanks the many individuals who contributed to its work. The people who briefed the committee at the workshop and in subsequent meetings are listed in Appendix B; we appreciated their willingness to address the questions we posed to them and are grateful for their insights. The sponsors of the report have been most supportive and responsive in helping the committee to do its work. The reviewers and the review monitor, listed below, provided thoughtful and detailed critiques that influenced the final form of the report significantly.
My personal thanks to Martyn Thomas, who from the start took a leading role in helping to crystallize the committee’s thinking and shared much of the burden of writing and editing the report; to Lynette Millett, our study director, for her constructive guidance throughout, for keeping us focused, and for her expert editing of the report; to associate program officer David Padgham for his meticulous help with the preparation of the final version; to our research associate at the start of the study, Phil Hilliard, for gathering materials and setting up our infrastructure; to my doctoral student, Derek Wayside, for configuring and maintaining the committee Wiki; to Liz Fikre of the DEPS editorial staff for her careful and clarifying assistance with manuscript preparation; to review monitor Elsa Garmire for her thorough and helpful oversight; and to Jon Eisenberg, director of the CSTB, for the special interest he has taken in this study and the attention and sage advice he has given.
Daniel Jackson, Chair
Committee on Certifiably Dependable Software Systems
Acknowledgment of Reviewers
This report has been reviewed in draft form by individuals chosen for their diverse perspectives and technical expertise, in accordance with procedures approved by the National Research Council’s (NRC’s) Report Review Committee. The purpose of this independent review is to provide candid and critical comments that will assist the institution in making its published report as sound as possible and to ensure that the report meets institutional standards for objectivity, evidence, and responsiveness to the study charge. The review comments and draft manuscript remain confidential to protect the integrity of the deliberative process. We wish to thank the following individuals for their review of this report:
Ashish Arora, Carnegie Mellon University,
David Corman, Boeing Company,
Steven Fenves, Carnegie Mellon University,
R. John Hansman, Massachusetts Institute of Technology,
Butler Lampson, Microsoft Corporation,
Jesse H. Poore, University of Tennessee,
Tariq Samad, Honeywell Automation and Control Solutions,
Alfred Z. Spector, Independent Consultant, and
William Stead, Vanderbilt University.
Although the reviewers listed above have provided many constructive comments and suggestions, they were not asked to endorse the con-
clusions or recommendations, nor did they see the final draft of the report before its release. The review of this report was overseen by Elsa Garmire of Dartmouth University. Appointed by the NRC, she was responsible for making certain that an independent examination of this report was carried out in accordance with institutional procedures and that all review comments were carefully considered. Responsibility for the final content of this report rests entirely with the authoring committee and the institution.