{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T17:01:55Z","timestamp":1725642115085},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540559603"},{"type":"electronic","value":"9783642778100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/978-3-642-77810-0_9","type":"book-chapter","created":{"date-parts":[[2011,12,9]],"date-time":"2011-12-09T20:17:31Z","timestamp":1323461851000},"page":"117-131","source":"Crossref","is-referenced-by-count":0,"title":["Developing Complex Software for Critical Systems"],"prefix":"10.1007","author":[{"given":"Peter G.","family":"Neumann","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness","author":"M Abadi","year":"1989","unstructured":"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\u201341."},{"issue":"4","key":"9_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"B. Alpern and F. B. Schneider (1985). Defining liveness. Information Processing Letters, 21 (4=Oct):181\u2013185.","journal-title":"Information Processing Letters"},{"issue":"l","key":"9_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/356901.356903","volume":"15","author":"GR Andrews","year":"1983","unstructured":"G.R. Andrews and F.B. Schneider (1983) Concepts and notations for concurrent programming. ACM Computing Surveys, 15(l=Mar):3\u201343.","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/356842.356846","volume":"13","author":"PA Bernstein","year":"1981","unstructured":"P.A. Bernstein and N. Goodman (1981) Concurrency control in distributed database systems. ACM Computing Surveys, 13(2=Jun):185\u2013221.","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"9_CR5","first-page":"519","volume":"5","author":"WR Bevier","year":"1989","unstructured":"W.R. Bevier (1989) Kit and the short stack. Journal of Automated Reasoning, 5(4=Dec):519\u201330.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"9_CR6","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"WR Bevier","year":"1989","unstructured":"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\u201328.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR7","series-title":"Final Draft, version 2.0.","volume-title":"Canadian Trusted Computer Product Evaluation Criteria","author":"CTCPEC","year":"1990","unstructured":"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."},{"key":"9_CR8","first-page":"43","volume-title":"Programming Languages","author":"EW Dijkstra","year":"1968","unstructured":"E.W. Dijkstra (1968a) Co-operating sequential processes. In F. Genuys (editor), Programming Languages, Academic Press, 43\u2013112."},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/363095.363143","volume":"11","author":"EW Dijkstra","year":"1968","unstructured":"E.W. Dijkstra (1968b) The structure of the THE multiprogramming system. Comm. ACM, 11(5=May), 341\u2013346.","journal-title":"Comm. ACM"},{"key":"9_CR10","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"E.W. Dijkstra (1976) A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"9_CR11","first-page":"329","volume-title":"Proc. National Computer Confi.","author":"RJ Feiertag","year":"1979","unstructured":"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\u2013334."},{"key":"9_CR12","series-title":"Tech Report CSL-109","volume-title":"Computer Science Laboratory","author":"RJ Feiertag","year":"1980","unstructured":"R.J. Feiertag (1980) A technique for proving specifications are multilevel secure. Tech Report CSL-109, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"9_CR13","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"C.A.R. Hoare (1985) Communicating Sequential Processes. Prentice-Hall."},{"issue":"4","key":"9_CR14","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"WA Hunt Jr","year":"1989","unstructured":"W.A. Hunt Jr. (1989) Microprocessor design verification. Journal of Automated Reasoning, 5(4):429\u2013460.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR15","volume-title":"Information Technology Security Evaluation Criteria (ITSEC), Provisional Harmonised Criteria (of France, Germany, the Netherlands, and the United Kingdom)","author":"ITSEC","year":"1991","unstructured":"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\u2013826\u20133004\u20138, available from the Office for Official Publications of the European Communities, L-2985 Luxembourg, item CD-71\u201391\u2013502-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."},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"L. Lamport, R. Shostak, and M. Pease (1982) The Byzantine generals problem. ACM TOPLAS, 4(3=Jul):382\u2013401.","journal-title":"ACM TOPLAS"},{"issue":"l","key":"9_CR17","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L Lamport","year":"1989","unstructured":"L. Lamport (1989) A simple approach to specifying concurrent program systems. Comm. ACM, 32(l=Jan):32\u201345.","journal-title":"Comm. ACM"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1145\/7474.7528","volume":"18","author":"NG Leveson","year":"1986","unstructured":"N.G. Leveson (1986) Software safety: Why, what and how. ACM Computing Surveys, 18(2=Jun):125\u2013163.","journal-title":"ACM Computing Surveys"},{"issue":"6","key":"9_CR19","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1109\/32.55088","volume":"16","author":"TF Lunt","year":"1990","unstructured":"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\u2013607.","journal-title":"IEEE Trans. Software Engineering"},{"key":"9_CR20","series-title":"Tech Report CSL-92\u201305","volume-title":"Computer Science Laboratory","author":"TF Lunt","year":"1992","unstructured":"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\u201305, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"issue":"4","key":"9_CR21","first-page":"461","volume":"5","author":"JS Moore","year":"1989","unstructured":"J S. Moore (1989a) A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461\u201392.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"9_CR22","first-page":"409","volume":"5","author":"JS Moore","year":"1989","unstructured":"J S. Moore (1989b) System verification. Journal of Automated Reasoning, 5(4):409\u2013410.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR23","series-title":"Contractor Report 4097","volume-title":"Design verification of SIFT","author":"L Moser","year":"1987","unstructured":"L. Moser, P.M. Melliar-Smith, and R. Schwartz (1987) Design verification of SIFT. Contractor Report 4097, NASA Langley Research Center, Hampton, VA."},{"key":"9_CR24","volume-title":"Department of Defense Trusted Computer System Evaluation Criteria (TCSEC)","author":"NCSC-TCSEC","year":"1985","unstructured":"NCSC-TCSEC (1985) Department of Defense Trusted Computer System Evaluation Criteria (TCSEC). National Computer Security Center. DOD-5200.28-STD, Orange Book."},{"key":"9_CR25","volume-title":"Guidance for Applying the Trusted Computer System Evaluation Criteria in Specific Environments","author":"NCSC-TCSECG","year":"1985","unstructured":"NCSC-TCSECG (1985) Guidance for Applying the Trusted Computer System Evaluation Criteria in Specific Environments. National Computer Security Center. CSC-STD-003\u201385."},{"key":"9_CR26","volume-title":"Trusted Network Interpretation (TNI)","author":"NCSC-TNI","year":"1990","unstructured":"NCSC-TNI (1990) Trusted Network Interpretation (TNI). National Computer Security Center. NCSC-TG-011 Version-1, Red Book."},{"key":"9_CR27","volume-title":"Trusted Network Interpretation Environments Guideline","author":"NCSC-TNIG","year":"1990","unstructured":"NCSC-TNIG (1990) Trusted Network Interpretation Environments Guideline. National Computer Security Center. NCSC-TG-011 Version-1."},{"key":"9_CR28","volume-title":"Trusted Database Management System Interpretation of the Trusted Computer System Evaluation Criteria (TDI)","author":"NCSC-TDI","year":"1991","unstructured":"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."},{"key":"9_CR29","first-page":"52","volume-title":"4. Jahrestagung der GI","author":"PG Neumann","year":"1974","unstructured":"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\u201366."},{"issue":"9","key":"9_CR30","doi-asserted-by":"crossref","first-page":"905","DOI":"10.1109\/TSE.1986.6313046","volume":"12","author":"PG Neumann","year":"1986","unstructured":"P.G. Neumann (1986) On hierarchical design of computer systems for critical applications. IEEE Trans. Software Engineering, SE-12(9=Sep):905\u2013920. Reprinted in Rein Turn (editor), Advances in Computer System Security, 3, Artech House, Dedham MA, 1988.","journal-title":"IEEE Trans. Software Engineering"},{"key":"9_CR31","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/978-1-4612-4476-9_40","volume-title":"Beauty is our Business, A Birthday Salute to Edsger W. Dijkstra","author":"PG Neumann","year":"1990","unstructured":"P.G. Neumann (1990a) Beauty and the beast of software complexity \u2014 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\u2013351. (ISBN 0\u2013387\u201397299\u20134)."},{"key":"9_CR32","first-page":"173","volume-title":"Proc. 5th Annual Conference on Computer Assurance, COMPASS 50","author":"PG Neumann","year":"1990","unstructured":"P.G. Neumann (1990b) The computer-related risk of the year: Distributed control. In Proc. 5th Annual Conference on Computer Assurance, COMPASS 50:173\u2013177. (IEEE 90CH2830)"},{"key":"9_CR33","series-title":"Tech Report CSL-90\u201310","volume-title":"On the design of dependable computer systems for critical applications","author":"PG Neumann","year":"1990","unstructured":"P.G. Neumann (1990c) On the design of dependable computer systems for critical applications. Tech Report CSL-90\u201310, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/CMPASS.1991.161027","volume-title":"Proc. 6th Annual Conference on Computer Assurance, COMPASS 91","author":"PG Neumann","year":"1991","unstructured":"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\u20138. (IEEE 91CH3033\u20138)"},{"key":"9_CR35","volume-title":"Managing Complexity and Modeling Reality: Strategic Issues and an Action Agenda","author":"PG Neumann","year":"1991","unstructured":"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\u201336 \u2013 2\u201342. (ISBN 0\u201389791\u2013458\u20139)"},{"issue":"l","key":"9_CR36","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/134292.134293","volume":"17","author":"PG Neumann","year":"1992","unstructured":"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\u201332. (At-least-quarterly cumulative updates to this index are available on request, including more recent references.)","journal-title":"ACM Software Engineering Notes"},{"key":"9_CR37","first-page":"396","volume-title":"Proc. 12th National Computer Security Conference","author":"PG Neumann","year":"1989","unstructured":"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\u2013407."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"D.L. Pamas (1972) On the criteria to be used in decomposing systems into modules. Comm. ACM, 15(12=Dec).","DOI":"10.1145\/361598.361623"},{"key":"9_CR39","first-page":"336","volume-title":"Information Processing 74","author":"DL Parnas","year":"1974","unstructured":"D.L. Parnas (1974) On a \u2018buzzword\u2019: Hierarchical structure. In Information Processing 74 (IFIP, Software:336\u2013339. North-Holland Publishing Co."},{"key":"9_CR40","series-title":"Tech Report","volume-title":"Sea View formal specifications","author":"NE Proctor","year":"1991","unstructured":"N.E. Proctor (1991) Sea View formal specifications. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"issue":"4","key":"9_CR41","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359461.359483","volume":"20","author":"L Robinson","year":"1977","unstructured":"L. Robinson and K.N. Levitt (1977) Proof techniques for hierarchically structured programs. Comm. ACM, 20(4=Apr):271\u2013283.","journal-title":"Comm. ACM"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"E. Rosen (1981) Vulnerabilities of network control protocols. ACM SIGSOFT","DOI":"10.17487\/rfc0789"},{"key":"9_CR43","unstructured":"Software Engineering Notes, 6(l=Jan):6\u20138."},{"key":"9_CR44","series-title":"Tech Report","volume-title":"Verifying noninterference security policies","author":"JM Rushby","year":"1989","unstructured":"J.M. Rushby (1989a) Verifying noninterference security policies. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"9_CR45","first-page":"210","volume-title":"Safe and Secure Computing Systems","author":"JM Rushby","year":"1989","unstructured":"J.M. Rushby (1989b) Kernels for safety? In T. Anderson, editor, Safe and Secure Computing Systems, Blackwell Scientific Publications, Chapter 13:210 \u2013 220 (Proceedings of a Symposium held in Glasgow, October 1986)."},{"key":"9_CR46","series-title":"Tech Report","volume-title":"Composing trustworthy systems","author":"JM Rushby","year":"1991","unstructured":"J.M. Rushby (1991) Composing trustworthy systems. Tech Report, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"issue":"5","key":"9_CR47","doi-asserted-by":"publisher","first-page":"l","DOI":"10.1145\/123041.123044","volume":"16","author":"JM Rushby","year":"1991","unstructured":"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 \u203291, Software for Critical Systems).","journal-title":"ACM Software Engineering Notes"},{"key":"9_CR48","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1109\/ECBS.1988.5465","volume-title":"Proc. Symposium on the Engineering of Computer-Based Medical Systems","author":"D Santel","year":"1988","unstructured":"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\u2013154, IEEE Computer Society."},{"key":"9_CR49","volume-title":"Interim Defence Standard 00\u201355, The Procurement of Safety Critical Software in Defence Equipment","author":"UK-MoD","year":"1991","unstructured":"UK-MoD (1991a) Interim Defence Standard 00\u201355, The Procurement of Safety Critical Software in Defence Equipment U.K. Ministry of Defence. (DefStan 00\u201355, Part 1, Issue 1: Requirements; Part 2, Issue 1: Guidance.)"},{"key":"9_CR50","volume-title":"Interim Defence Standard 00\u201356, Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment","author":"UK-MoD","year":"1991","unstructured":"UK-MoD (1991b) Interim Defence Standard 00\u201356, Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment. U.K. Ministry of Defence. (DefStan 00\u201356)."},{"key":"9_CR51","volume-title":"Introduction to Ehdm","author":"F Henke von","year":"1988","unstructured":"F. von Henke and J.M. Rushby (1988) Introduction to Ehdm. Computer Science Laboratory, SRI International, Menlo Park, CA 94025"},{"issue":"4","key":"9_CR52","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W.D. Young","year":"1989","unstructured":"W.D. Young (1989) A mechanically verified code generator. Journal of Automated Reasoning, 5(4):493\u2013518.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Informatik aktuell","Information als Produktionsfaktor"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-77810-0_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,6]],"date-time":"2021-05-06T12:55:41Z","timestamp":1620305741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-77810-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540559603","9783642778100"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-77810-0_9","relation":{},"ISSN":["1431-472X"],"issn-type":[{"type":"print","value":"1431-472X"}],"subject":[],"published":{"date-parts":[[1992]]}}}