SOFTWARE FOR DEPENDABLE SYSTEMS

SUFFICIENT EVIDENCE?

Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors

Committee on Certifiably Dependable Software Systems

Computer Science and Telecommunications Board

Division on Engineering and Physical Sciences


NATIONAL RESEARCH COUNCIL OF THE NATIONAL ACADEMIES

THE NATIONAL ACADEMIES PRESS

Washington, D.C.
www.nap.edu



The National Academies | 500 Fifth St. N.W. | Washington, D.C. 20001
Copyright © National Academy of Sciences. All rights reserved.
Terms of Use and Privacy Statement



Below are the first 10 and last 10 pages of uncorrected machine-read text (when available) of this chapter, followed by the top 30 algorithmically extracted key phrases from the chapter as a whole.
Intended to provide our own search engines and external engines with highly rich, chapter-representative searchable text on the opening pages of each chapter. Because it is UNCORRECTED material, please consider the following text as a useful but insufficient proxy for the authoritative book pages.

Do not use for reproduction, copying, pasting, or reading; exclusively for search engines.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? SOFTWARE FOR DEPENDABLE SYSTEMS SUFFICIENT EVIDENCE? Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors Committee on Certifiably Dependable Software Systems Computer Science and Telecommunications Board Division on Engineering and Physical Sciences NATIONAL RESEARCH COUNCIL OF THE NATIONAL ACADEMIES THE NATIONAL ACADEMIES PRESS Washington, D.C. www.nap.edu

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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. www.national-academies.org

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? This page intentionally left blank.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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)

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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 1 The committee uses the term “certification” to refer to the process of assuring that a product or process has certain stated properties, which are then recorded in a certificate. Certification usually involves assurance by an independent party, although the term is also used analogously for customer (second-party) and developer (first-party) assurance.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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/>.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? This page intentionally left blank.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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-

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 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.

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? Contents     SUMMARY   1 1   ASSESSMENT: SOFTWARE SYSTEMS AND DEPENDABILITY TODAY   16      Cost and Schedule Challenges in Software Development,   17      Disruptions and Accidents Due to Software,   18      Hazardous Materials,   20      Aviation,   21      Medical Devices and Systems,   23      Infrastructure,   26      Defense,   27      Distribution of Energy and Goods,   28      Voting,   29      Problems with Existing Certification Schemes,   29      Security Certification,   30      Avionics Certification,   33      Medical Software Certification,   35      Opportunities for Dependable Software,   36      Air Transportation,   37      Medicine,   37      Observations,   38      Observation 1: Lack of Evidence,   39      Observation 2: Not Just Bugs,   40      Observation 3: The Cost of Strong Approaches,   41

OCR for page R1
Software For Dependable Systems: Sufficient Evidence?      Observation 4: Coupling and Complexity,   45      Observation 5: Safety Culture Matters,   48 2   PROPOSED APPROACH   51      Explicit Dependability Claims,   54      What Is Dependability?,   54      Why Claims Must Be Explicit,   55      Software as a System Component,   56      Accidental Systems and Criticality Creep,   57      Evolution and Recertification,   59      What to Make Explicit,   60      Requirements, Specifications, and Domain Assumptions,   61      Evidence,   66      Goal-Based Versus Process-Based Assurance,   66      The Dependability Case,   68      The Role of Domain Assumptions,   68      The Role of Architecture,   69      The Role of Testing,   70      The Role of Analysis,   74      Rigorous Process: Preserving the Chain of Evidence,   75      Components and Reuse,   76      Expertise,   78      Simplicity,   79      Best Practices,   83      Feasibility of the Overall Approach,   87 3   BROADER ISSUES   89      Transparency,   89      Accountability and Liability,   91      Certification,   92      Evidence and Openness,   93      Security Concerns,   94      A Repository of Software Dependability Data,   96      Education,   97      Research,   99 4   FINDINGS AND RECOMMENDATIONS   103      Findings,   103      Recommendations,   104      To Builders and Users of Software,   104      To Agencies and Organizations That Support Software Education and Research,   107

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? 5   BIBLIOGRAPHY   110     APPENDIXES          A  BIOGRAPHIES OF COMMITTEE MEMBERS AND STAFF   119      B  OPEN SESSION BRIEFERS   128      C  STATEMENT OF TASK   130

OCR for page R1
Software For Dependable Systems: Sufficient Evidence? This page intentionally left blank.