Skip to main content
SpringerLink
Log in

Developing Complex Software for Critical Systems

  • Conference paper
Book cover Information als Produktionsfaktor

Part of the book series: Informatik aktuell ((INFORMAT))

  • 364 Accesses

Abstract

There is a huge gap between the theories of computing and the practice of developing applications that must satisfy extremely critical application requirements such as human safety and mission survivability — which in turn may impose stringent demands for computer and communication system reliability, availability, security, integrity, real-time responsiveness, and (in many cases) correctness of the application software. Experience shows that such systems are vulnerable to a wide variety of misfortunes — including malicious misuse (by insiders and outsiders), hardware faults, software flaws, development malpractice, and ‘acts of God’ — with potentially devastating consequences. The challenge is to ensure that development efforts can address these problems, while at the same time recognizing the implications of certain intrinsic limitations, both technological and social.

This paper addresses system requirements, known types of vulnerabilities, past crises that illustrate the difficulties encountered, some constructive techniques for developing dependable systems, and various remaining concerns. Special emphasis is placed on effective structuring of requirements, system designs, and software developments, coordinated under a suitably generalized system perspective capable of transcending narrowly conceived requirements.

No one sees further into a generalization than his own knowledge of details extends.

William James

Presented at the 22. Jahrestagung der Gesellschaft für Informatik (GI), 30 September – 2 Oktober 1992, Karlsruhe, Germany.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • M. Abadi and L. Lamport (1989) Composing specifications. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, Springer-Verlag, Lecture Notes in Computer Science, vol. 230, 1–41.

    Google Scholar 

  • B. Alpern and F. B. Schneider (1985). Defining liveness. Information Processing Letters, 21 (4=Oct):181–185.

    Article  MATH  MathSciNet  Google Scholar 

  • G.R. Andrews and F.B. Schneider (1983) Concepts and notations for concurrent programming. ACM Computing Surveys, 15(l=Mar):3–43.

    Article  MATH  Google Scholar 

  • P.A. Bernstein and N. Goodman (1981) Concurrency control in distributed database systems. ACM Computing Surveys, 13(2=Jun):185–221.

    Article  MathSciNet  Google Scholar 

  • W.R. Bevier (1989) Kit and the short stack. Journal of Automated Reasoning, 5(4=Dec):519–30.

    Google Scholar 

  • W.R. Bevier, W.A. Hunt, Jr., J S. Moore, and W.D. Young (1989) An approach to systems verification. Journal of Automated Reasoning, 5(4):411–28.

    Google Scholar 

  • CTCPEC (1990) Canadian Trusted Computer Product Evaluation Criteria. Canadian Systems Security Centre, Communications Security Establishment, Government of Canada. Final Draft, version 2.0. (A 1992 draft version 3.0 is under review.

    Google Scholar 

  • E.W. Dijkstra (1968a) Co-operating sequential processes. In F. Genuys (editor), Programming Languages, Academic Press, 43–112.

    Google Scholar 

  • E.W. Dijkstra (1968b) The structure of the THE multiprogramming system. Comm. ACM, 11(5=May), 341–346.

    Article  MATH  Google Scholar 

  • E.W. Dijkstra (1976) A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.

    MATH  Google Scholar 

  • R.J. Feiertag and P.G. Neumann (1979) The foundations of a provably secure operating system (PSOS). In Proc. National Computer Confi., AFIPS Press, 329–334.

    Google Scholar 

  • R.J. Feiertag (1980) A technique for proving specifications are multilevel secure. Tech Report CSL-109, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • C.A.R. Hoare (1985) Communicating Sequential Processes. Prentice-Hall.

    MATH  Google Scholar 

  • W.A. Hunt Jr. (1989) Microprocessor design verification. Journal of Automated Reasoning, 5(4):429–460.

    Article  Google Scholar 

  • ITSEC (1991) Information Technology Security Evaluation Criteria (ITSEC), Provisional Harmonised Criteria (of France, Germany, the Netherlands, and the United Kingdom), European Communities Commission. Version 1.2, ISBN 92–826–3004–8, available from the Office for Official Publications of the European Communities, L-2985 Luxembourg, item CD-71–91–502-EN-C, or UK CLEF, CESG Room 2/0805, Fiddlers Green Lane, Cheltenham UK GLOS GL52 5AJ, or GSA/GISA, Am Nippenkreuz 19, D 5300 Bonn 2, Germany.

    Google Scholar 

  • L. Lamport, R. Shostak, and M. Pease (1982) The Byzantine generals problem. ACM TOPLAS, 4(3=Jul):382–401.

    Article  MATH  Google Scholar 

  • L. Lamport (1989) A simple approach to specifying concurrent program systems. Comm. ACM, 32(l=Jan):32–45.

    Article  MathSciNet  Google Scholar 

  • N.G. Leveson (1986) Software safety: Why, what and how. ACM Computing Surveys, 18(2=Jun):125–163.

    Article  Google Scholar 

  • T.F. Lunt, D.E. Denning, R.R. Schell, M. Heckman, and W.R. Shockley (1990) The SeaView security model. IEEE Trans. Software Engineering, 16(6=Jun):593–607.

    Article  Google Scholar 

  • T.F. Lunt, A. Tamaru, F. Gilham, R. Jagannathan, C. Jalali, P.G. Neumann, H.S. Javitz, and A. Valdes (1992) A real-time intrusion-detection expert system (IDES). Tech Report CSL-92–05, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • J S. Moore (1989a) A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461–92.

    Google Scholar 

  • J S. Moore (1989b) System verification. Journal of Automated Reasoning, 5(4):409–410.

    Google Scholar 

  • L. Moser, P.M. Melliar-Smith, and R. Schwartz (1987) Design verification of SIFT. Contractor Report 4097, NASA Langley Research Center, Hampton, VA.

    Google Scholar 

  • NCSC-TCSEC (1985) Department of Defense Trusted Computer System Evaluation Criteria (TCSEC). National Computer Security Center. DOD-5200.28-STD, Orange Book.

    Google Scholar 

  • NCSC-TCSECG (1985) Guidance for Applying the Trusted Computer System Evaluation Criteria in Specific Environments. National Computer Security Center. CSC-STD-003–85.

    Google Scholar 

  • NCSC-TNI (1990) Trusted Network Interpretation (TNI). National Computer Security Center. NCSC-TG-011 Version-1, Red Book.

    Google Scholar 

  • NCSC-TNIG (1990) Trusted Network Interpretation Environments Guideline. National Computer Security Center. NCSC-TG-011 Version-1.

    Google Scholar 

  • NCSC-TDI (1991) Trusted Database Management System Interpretation of the Trusted Computer System Evaluation Criteria (TDI). National Computer Security Center. NCSC-TG-021, Version-2, Lavender Book.

    Google Scholar 

  • P.G. Neumann (1974) Toward a methodology for designing large systems and verifying their properties. In 4. Jahrestagung der GI, Springer-Verlag, Lecture Notes in Computer Science, vol. 26:52–66.

    Google Scholar 

  • P.G. Neumann (1986) On hierarchical design of computer systems for critical applications. IEEE Trans. Software Engineering, SE-12(9=Sep):905–920. Reprinted in Rein Turn (editor), Advances in Computer System Security, 3, Artech House, Dedham MA, 1988.

    Google Scholar 

  • P.G. Neumann (1990a) Beauty and the beast of software complexity — elegance versus elephants. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra (editors), Beauty is our Business, A Birthday Salute to Edsger W. Dijkstra (11 May 1990), Springer-Verlag, Chapter 39:346–351. (ISBN 0–387–97299–4).

    Google Scholar 

  • P.G. Neumann (1990b) The computer-related risk of the year: Distributed control. In Proc. 5th Annual Conference on Computer Assurance, COMPASS 50:173–177. (IEEE 90CH2830)

    Google Scholar 

  • P.G. Neumann (1990c) On the design of dependable computer systems for critical applications. Tech Report CSL-90–10, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • P.G. Neumann (1991a) The computer-related risk of the year: Weak links and correlated events. In Proc. 6th Annual Conference on Computer Assurance, COMPASS 91, NIST:5–8. (IEEE 91CH3033–8)

    Chapter  Google Scholar 

  • P.G. Neumann (1991b) Managing complexity in critical systems. In D. Frailey (editor), Managing Complexity and Modeling Reality: Strategic Issues and an Action Agenda, ACM, New York, NY: 2–36 – 2–42. (ISBN 0–89791–458–9)

    Google Scholar 

  • P.G. Neumann (1992) Illustrative risks to the public in the use of computer systems and related technology: index to RISKS cases as of 23 December 1991. ACM Software Engineering Notes, 17(l=Jan):23–32. (At-least-quarterly cumulative updates to this index are available on request, including more recent references.)

    Article  Google Scholar 

  • P.G. Neumann and D.B. Parker (1989) A summary of computer misuse techniques. In Proc. 12th National Computer Security Conference, Baltimore, MD, NIST/NCSC:396–407.

    Google Scholar 

  • D.L. Pamas (1972) On the criteria to be used in decomposing systems into modules. Comm. ACM, 15(12=Dec).

    Google Scholar 

  • D.L. Parnas (1974) On a ‘buzzword’: Hierarchical structure. In Information Processing 74 (IFIP, Software:336–339. North-Holland Publishing Co.

    Google Scholar 

  • N.E. Proctor (1991) Sea View formal specifications. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • L. Robinson and K.N. Levitt (1977) Proof techniques for hierarchically structured programs. Comm. ACM, 20(4=Apr):271–283.

    Article  MATH  MathSciNet  Google Scholar 

  • E. Rosen (1981) Vulnerabilities of network control protocols. ACM SIGSOFT

    Google Scholar 

  • Software Engineering Notes, 6(l=Jan):6–8.

    Google Scholar 

  • J.M. Rushby (1989a) Verifying noninterference security policies. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • J.M. Rushby (1989b) Kernels for safety? In T. Anderson, editor, Safe and Secure Computing Systems, Blackwell Scientific Publications, Chapter 13:210 – 220 (Proceedings of a Symposium held in Glasgow, October 1986).

    Google Scholar 

  • J.M. Rushby (1991) Composing trustworthy systems. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA.

    Google Scholar 

  • J.M. Rushby and F. von Henke (1991) Formal verification of algorithms for critical systems. ACM Software Engineering Notes, 16(5=Dec):l-15 (Proc. SIGSOFT ′91, Software for Critical Systems).

    Article  Google Scholar 

  • D. Santel, C. Trautmann, and W. Liu (1988) The integration of a formal safety analysis into the software engineering process: An example from the pacemaker industry. In Proc. Symposium on the Engineering of Computer-Based Medical Systems, Minneapolis, MN:152–154, IEEE Computer Society.

    Chapter  Google Scholar 

  • UK-MoD (1991a) Interim Defence Standard 00–55, The Procurement of Safety Critical Software in Defence Equipment U.K. Ministry of Defence. (DefStan 00–55, Part 1, Issue 1: Requirements; Part 2, Issue 1: Guidance.)

    Google Scholar 

  • UK-MoD (1991b) Interim Defence Standard 00–56, Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment. U.K. Ministry of Defence. (DefStan 00–56).

    Google Scholar 

  • F. von Henke and J.M. Rushby (1988) Introduction to Ehdm. Computer Science Laboratory, SRI International, Menlo Park, CA 94025

    Google Scholar 

  • W.D. Young (1989) A mechanically verified code generator. Journal of Automated Reasoning, 5(4):493–518.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA, 94025-3493, USA

    Peter G. Neumann (Principal Scientist)

Authors
  1. Peter G. Neumann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut fü Rechnerentwurf und Fehlertoleranz, Universität Karlsruhe, Postfach 6980, W-7500, Karlsruhe 1, Germany

    Winfried Görke

  2. Hauptabteilung Ingenieurtechnik, Kernforschungszentrum Karlsruhe GmbH, Postfach 3640, W-7500, Karlsruhe 1, Germany

    Hermann Rininsland

  3. Fraunhofer Gesellschaft zur Förderung der angewandten Forschung e.V., Leonrodstraße 54, W-8000, München 19, Germany

    Max Syrbe

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Neumann, P.G. (1992). Developing Complex Software for Critical Systems. In: Görke, W., Rininsland, H., Syrbe, M. (eds) Information als Produktionsfaktor. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-77810-0_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-77810-0_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55960-3

  • Online ISBN: 978-3-642-77810-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation