RISKS-LIST: RISKS-FORUM Digest Weds 18 December 1991 Volume 12 : Issue BOWEN FORUM ON RISKS TO THE PUBLIC IN COMPUTERS AND RELATED SYSTEMS ACM Committee on Computers and Public Policy, Peter G. Neumann, moderator ---------------------------------------------------------------------- Date: Wed, 4 Dec 91 16:54:37 GMT From: Jonathan.Bowen@prg.oxford.ac.uk Subject: Software safety, formal methods and standards Peter, Below is an edited version of the messages I received back from my request in this area. I have posted this to the comp.software-eng and comp.specification newsgroups. This is probably too long for comp.risks, but perhaps it would be worth including a pointer to these two newsgroups. I hope you had a successful SIGSOFT conference. Will you be summarising what happened in comp.risks? I think this would be a useful service if you have the time. Jonathan Bowen, PRG, Oxford. Newsgroups: comp.software-eng,comp.specification Subject: Software safety, formal methods and standards Here is an edited (!) version of the messages I received back from my request for information in this area. I have only included messages I think are most relevant and have removed some sections of included messages (indicated by "..." below). Thank you for your responses. They have certainly been useful, and acknowledgements will be included where appropriate. Jonathan Bowen, Oxford University Computing Laboratory, UK. ------------------------------ Original message (RISKS-12.60, 6 November 1991): From: bowen@prg.ox.ac.uk (Jonathan Bowen) Subject: Software safety, formal methods and standards Date: 6 Nov 91 12:29:45 GMT Reply-To: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen) Organization: Programming Research Group, Oxford University, UK I am writing a review paper on software safety, formal methods and standards. In particular, I am looking at the recommendations for the use of formal methods in software safety standards (and draft standards). So far I have considered the (some draft) standards listed below. If anyone has any recommendations of others to consider, please send me details of how to obtain them (or the document itself if possible!). I am also interested in general references in this area. I have quite a few already, but I may have missed some. If they are obscure and you can send me the paper itself, so much the better. If there is enough interest, I will summarize the responses. -- Jonathan Bowen Oxford University Computing Laboratory, Programming Research Group 11 Keble Road, Oxford OX1 3QD, England. Tel: +44-865-272574 (direct) or 273840 (secretary) FAX: +44-865-272582 (direct) or 273839 (general) Email: Jonathan.Bowen@comlab.ox.ac.uk ------------------------------ ESA software engineering standards, European Space Agency, 8-10 rue Mario-Nikis, 75738 Paris Cedex, France, ESA PSS-05-0 Issue 2, February 1991. Programmable Electronic Systems in Safety Related Applications: 1. An Introductory Guide, Health and Safety Executive, HMSO, Publications Centre, PO Box 276, London SW8 5DT, UK, 1987. Programmable Electronic Systems in Safety Related Applications: 2. General Technical Guidelines, Health and Safety Executive, HMSO, Publications Centre, PO Box 276, London SW8 5DT, UK, 1987. Software for computers in the application of industrial safety related systems, International Electrotechnical Commission, Technical Committee no. 65, 1989. (BS89/33006DC) Functional safety of programmable electronic systems: Generic aspects, International Electrotechnical Commission, Technical Committee no. 65, 1989. (BS89/33005DC) Standard for software safety plans, Preliminary - subject to revision, P1228, Software Safety Plans Working Group, Software Engineering Standards Subcommittee, IEEE Computer Society, USA, July 1991. The Procurement of Safety Critical Software in Defence Equipment (Part 1: Requirements, Part 2: Guidance), Interim Defence Standard 00-55, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK, 5 April 1991. Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment, Interim Defence Standard 00-56, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK, 5 April 1991. Safety related software for railway signalling, BRB/LU Ltd/RIA technical specification no. 23, Consultative Document, Railway Industry Association, 6 Buckingham Gate, London SW1E 6JP, UK, 1991. -- Jonathan Bowen, Oxford University Computing Laboratory. >From bld@gov.nasa.larc.air16 Wed Nov 6 18:41:43 1991 Message-Id: <9111061545.AA15591@air57.larc.nasa.gov> Date: Wed, 6 Nov 91 10:45:28 -0500 From: "Ben L. Di Vito" To: Jonathan Bowen In-Reply-To: bowen@prg.ox.ac.uk's message of 6 Nov 91 12:29:45 GMT Subject: Software safety, formal methods and standards Reply-To: bld@gov.nasa.larc.air12 In the US, software for civilian aircraft is certified in accordance with the DO-178A "standard" published by a professional organization known as RTCA: Software Considerations in Airborne Systems and Equipment Certification DO-178A March, 1985 Radio Technical Commission for Aeronautics One McPherson Square 1425 K Street N.W., Suite 500 Washington, D.C. 20005 Technically, this is only a "guideline" rather than a standard, but in practice the FAA tends to view it as having the weight of a standard. It states various requirements that should be met for software to be certified at three degrees of criticality. DO-178B is a revision currently being worked out in committee. It will probably hit the streets in about a year. George Finelli of NASA Langley Research Center in on the RCTA committee. He and I have been trying to insert some material on formal methods into the revised document (DO-178A does not explicitly recognize formal methods as part of accepted practice). Right now it looks like we will be able to get in one page of very general guidelines on using formal methods in a section on alternate means of compliance. Basically it suggests how one might be able to trade off formal methods against traditional kinds of verification to earn "certification credit." Unfortunately, it will not go nearly as far as 00-55 in embracing formal methods overall. If you would like to include something on DO-178B in your paper, check back with us in a few weeks. I'm not sure what can be said right now since this material I mentioned has not yet been approved by the full committee. Other standards in the US may also be of interest to you. You may have heard of the Trusted Computer System Evaluation Criteria published by the DoD. It is primarily concerned with computer security, but that community has been the leading proponent of applied formal methods here for over ten years. I have also heard of some proposed standards to be issued by the National Institute of Standards and Technology (NIST), formerly National Bureau of Standards (NBS). I think these are still too embryonic to talk about, though. ... Ben Di Vito Vigyan, Inc. bld@air12.larc.nasa.gov MS 130 NASA Langley Research Center (804) 864-4883 Hampton, VA 23665 USA >From steph%edu.uci.ics.rennes@edu.uci.ics.paris Wed Nov 6 21:29:54 1991 To: Jonathan.Bowen@prg Subject: Re: Software safety, formal methods and standards References: <2464@culhua.prg.ox.ac.uk> Date: Wed, 06 Nov 91 11:27:05 -0800 Message-Id: <14251.689455625@rennes.ics.uci.edu> From: steph@edu.uci.ics.rennes Sender: steph%edu.uci.ics.rennes@edu.uci.ics.paris ... You might want to look at these: ISO 9000 (sorry, forgot the title) I know the FDA (US Food and Drug Administration) has come up with some new guildlines recently too. -- Good luck, Stephanie Aha steph@ics.uci.edu Information and Computer Science U.C. Irvine, Irvine, CA 92717 USA >From bryan@edu.Stanford.asterix Thu Nov 7 01:20:25 1991 Thu, 7 Nov 1991 00:08:06 +0000 Date: Wed, 6 Nov 91 16:07:19 PST From: bryan@edu.Stanford.asterix (Douglas L. Bryan) Message-Id: <9111070007.AA02120@asterix.Stanford.EDU> To: Jonathan.Bowen@prg Subject: Re: Software safety, formal methods and standards Sender: bryan@edu.Stanford.asterix ``Proposed Standard for Software for Computers in the Safety Systems of Nuclear Power Stations'', (based on IEC Standard 880), Final Report for contract 2.117.1 for the Atomic Energy Control Board, March 1991. by David L. Parnas, TRIO, Computer and Information Science, Queen's University, Kington, Ontario K7L 3N6 Canada. ... I don't know that 2.117.1 or IEC mean, and I don't know if it's been published; I received a copy from a friend months ago. doug >From barriost%gtephx@net.eu.relay Thu Nov 7 23:21:32 1991 Message-Id: <9111071556.AA03664@gtephx.com> Subject: Re: Software safety, formal methods and standards To: Jonathan.Bowen@prg Date: Thu, 7 Nov 91 8:56:54 MST Cc: scott@uucp.ithaca Sender: barriost%gtephx@net.eu.relay ... A good friend of mine, Scott Sheppard, wrote his master's thesis on the subject of Software Safety (in 1989?). it would be available from the Arizona State University library. or, if you'd like to contact Scott, his email address is: uunet!ithaca!scott -- Tim Barrios, AG Communication Systems, Phoenix, AZ UUCP: ...!{ncar!noao!asuvax | uunet!samsung!romed!asuvax | att}!gtephx!barriost Internet: gtephx!barriost@asuvax.eas.asu.edu voice: (602) 582-7101 fax: (602) 581-4022 >From ramu%com.mot.corp.cadsun@com.mot.motgate Fri Nov 8 03:24:40 1991 From: ramu@com.mot.corp.cadsun Date: Wed, 6 Nov 91 16:30:10 CST Message-Id: <9111062230.AA14120@cadsun.corp.mot.com> To: Jonathan.Bowen@prg Cc: ramu@com.mot.corp.cadsun Subject: Re: Software safety, formal methods and standards References: <2464@culhua.prg.ox.ac.uk> Sender: ramu%com.mot.corp.cadsun@com.mot.motgate ... Hi! You may want to look at the NIST document on High Integrity Software. Details about obtaining it is at the end of the message. This is a very comprehensive report that discusses the topic about software safety, hazard analysis, and does include some references. This software is available via an archive-server. I think you've compiled a very useful list of software safety references. May I obtain additional information about obtaining the following document? An email address should suffice. >> Standard for software safety plans, >> Preliminary - subject to revision, >> P1228, Software Safety Plans Working Group, >> Software Engineering Standards Subcommittee, >> IEEE Computer Society, USA, July 1991. Another possibly useful reference would be in a journal called "Journal of Safety and Reliability" -- I remember that one of the issues, concentrating on software safety, was published as a book. I don't remember the exact year, but a trip to the library should solve the problem via browsing. Here's the information about the NIST document: Xref: motsrd comp.software-eng:4855 comp.specification:471 Path: motsrd!mothost!ftpbox!uunet!dove!swe.ncsl.nist.gov!kuhn From: kuhn@swe.ncsl.nist.gov (Rick Kuhn) Subject: Report on Assurance of High Integrity Software Message-ID: <951@dove.nist.gov> Date: 4 Oct 91 18:09:42 GMT Sender: news@dove.nist.gov Followup-To: comp.software-eng Organization: NIST Lines: 37 Assurance of High Integrity Software - report available The need for dependable software has resulted in the production of a variety of standards: the Trusted Computer Security Evaluation Criteria ("Orange Book"), the British MoD 00-55, the DO-178A standard for civil aviation, the IEC 880 standard for the nuclear industry, and others. Because of technical, economic, and political considerations, these standards approach the question of assurance from a variety of viewpoints. There is much disagreement over how dependable software can be produced. The controversy over MoD 00-55, with its requirement for formal methods and deprecated programming practices, is a recent example. To address the question of assuring the trustworthiness and integrity of software, and what assurances should be required in standards, the National Institute of Standards and Technology brought together experts from industry, academia, and government in a Workshop on the Assurance of High Integrity Software in January. The report is now available for electronic distribution. (It will soon be available from the Govt. Printing Office in paper form.) The report can be obtained from our mail server. Both Postscript and troff formats are available. Send a message containing ONE of the following requests to posix@nist.gov: send ahisrptp /* for Postscript */ send ahisrptt /* for troff */ The report will be delivered as three (troff) or 16 (postscript) email messages. Remove the headers and concatenate the files, then unpack them using either 'unshar' or the UNIX shell 'sh'. (Instructions included in the files.) Hope this helps. --Ramu Iyer ramu@mot.com >From steve@edu.ucar.unidata Fri Nov 8 05:15:41 1991 Date: Thu, 7 Nov 1991 21:48:32 -0700 From: Steve Emmerson Message-Id: <199111080448.AA06243@unidata.ucar.edu> To: Jonathan.Bowen@prg Subject: Re: Software safety, formal methods and standards [via Jim Horning] References: Organization: UCAR/Unidata ... (From my files:) >From comp.risks Tue Sep 4 20:05:34 1990 Date: Fri, 31 Aug 90 18:08:40 -0700 From: Nancy Leveson Subject: What is "safety-critical"? Reply-To: nancy@ics.UCI.EDU RISKS-10.28 was certainly provocative. I do not want to enter into the basic argument, but I would like to comment on a couple of statements that appear incorrect to me. Peter Mellor writes: >Safety-*related*, I would say, but not safety-*critical*. The usual >definition of safety-critical is that a system failure results in >catastrophe. System safety engineers in the textbooks I have read do not define "safety-critical" in terms of catastrophic failure. They use "hazards" and the ability to contribute to a hazard. A safety-critical system or subsystem is one that can contribute to the system getting into a hazardous state. There are very good reasons for this, which I will attempt to explain. Accidents do not usually have single causes -- most are multi-factorial. We usually eliminate the simpler accident potentials from our systems which only leaves multi-failure accidents. The basic system safety goal is to eliminate all single-point failures that could lead to unacceptable consequences and minimize the probability of accidents caused by multi-point failures. Using Pete`s definition, there are almost NO systems that are safety critical including nuclear power plant and air traffic control systems because we rarely build these systems so that a single failure of a single component can lead to an accident. That the failure of the whole nuclear power plant or air traffic "system" is an accident is tautological -- what we are really talking about are failures of components or subsystems of these larger "systems" like the control components or the simulators (in this case). The term "safety-related" seems unfortunate to me because it is too vague to be defined. Some U.S. standards talk about "first-level interfaces" (actions can directly contribute to a system hazard) or "second-level" (actions can adversely affect the operation of another component that can directly contribute to a hazard). Another way of handling this is to talk about likelihood of contributing to a hazard -- with the longer chains having a lower likelihood. But I would consider them all safety-critical if their behavior can contribute to a hazard -- it is only the magnitude of the risk that differs. I have a feeling that the term "safety-related" is often used to abdicate or lessen responsibility. There is a very practical reason for using hazards (states which in combination with particular environmental conditions have an unacceptable risk of leading to an accident). In most complex systems, the designer has no control over many of the conditions that could lead to an accident. For example, air traffic control hazards are stated in terms of minimum separation between aircraft (or near misses) rather than in terms of eliminating collisions (which, of course, is the ultimate goal). The reason is that whether a collision occurs depends not only on close proximity of the aircraft but also partly on pilot alertness, luck, weather, and a lot of other things that are not under the control of the designer of the system. So what can the designer do to reduce risk? She can control only the proximity hazard and that is what she does, i.e., assumes that the environment is in the worst plausible conditions (bad weather, pilot daydreaming) and attempts to keep the planes separated by at least 500 feet (or whatever, the exact requirements depend on the circumstances). When assessing the risk of the air traffic control system, the likelihood of the hazard, i.e., violation of minimum separation standards, is assessed, not the likelihood of an ATC-caused accident. When one later does a complete system safety assessment, the risk involved in this hazard along with the risk of the other contributory factors are combined into the risk of a collision. Why does this push my hot button? Well, I cannot tell you how many times I have been told that X system is not safety-critical because it's failure will not cause an accident. For example, a man from MITRE and the FAA argued with me that the U.S. air traffic control software is not safety critical (and therefore does not require any special treatment) because there is no possible failure of the software that could cause an accident. They argued that the software merely gives information to the controller who is the one who gives the pilot directions. If the software provides the wrong information to the controller, well there was always the chance that the controller or the pilot could have determined that it was wrong somehow. But an ATC software failure does not necessarily result in a catastrophe so it is not safety critical (as defined above). Perhaps this argument appeals to you, but as a person who flies a lot, I am not thrilled by it. As I said, this argument can be applied to EVERY system and thus, by the above definition, NO systems are safety-critical. Again, there may be disagreement, but I think the argument has been pushed to its absurd limit in commercial avionic software. The argument has been made by some to the FAA (and it is in DO-178A and will probably be in D0-178B) that reduction in criticality of software be allowed on the basis of the use of a protective device. That is, if you put in a backup system for autoland software, then the autoland system itself is not safety critical and need not be as thoroughly tested. (One could argue similarly that the backup system is also not safety-critical since it's failure alone will not cause an accident -- both of them must fail -- and therefore neither needs to be tested thoroughly. This argument is fine when you can accurately access reliability and thus can accurately combine the probabilities. But we have no measures for software reliability that provide adequate confidence at the levels required, as Pete says). The major reason for some to support allowing this reduction is that they want to argue that the use of n-version software reduces the criticality of the function provided by that software (none of the versions is safety critical because a failure in one alone will not lead to an accident) and therefore required testing and other quality assurance procedures for the software can be reduced. >With a safety-critical airborne system, we are certifying that it has >a certain maximum probability of crashing the aircraft. Actually, you are more likely to be certifying that it will not get into (or has a maximum probability of getting into) a hazardous state from which the pilot or a backup system cannot recover or has an unacceptably low probability of recovering. The distinction is subtle, but important as I argued above. Few airborn systems have the capacity to crash the aircraft by themselves (although we are heading in this direction and some do exist -- which violates basic system safety design principles). >RTCA/DO-178A ('Software Considerations in Airborne Systems and Equipment >Certification') does *not* define any reliability figures. It is merely a >set of guidelines defining quality assurance practices for software. >Regulatory approval depends upon the developer supplying certain documents >(e.g., software test plan, procedures and results) to show that the >guidelines have been followed. There is currently an effort to produce a DO-178B. This will go farther than 178A does. For one thing, it is likely to include the use of formal methods. Second, it will almost certainly require hazard-analysis procedures. If anyone is interested in attending these meetings and participating, they are open to the public and to all nationalities. >From Pete Mellor's description of the Forrester and Morrison article: >This is likely to change following the publication of the draft defence >standard 00-55 by the MoD in the UK in May 1989. The DoD in the US are >not doing anything similar, though the International Civil Aviation >Organisation is planning to go to formal methods. Depends on what you mean by similar. The DoD, in Mil-Std-882B (System Safety) has required formal analysis of software safety since the early 80s. MoD draft defense standard 00-56 requires less than the equivalent DoD standard. There has been a DoD standard called "Software Nuclear Safety" that has been in force for nuclear systems for about 4-5 years. And there are other standards requiring software safety analysis (e.g., for Air Force missile systems) that were supplanted by 882B. 882B is likely to be replaced by 882C soon -- and the accompanying handbooks, etc. do mention the use of formal methods to accomplish the software safety analysis tasks. nancy >From al@edu.nmt.jupiter Sat Nov 9 02:40:00 1991 Date: Thu, 7 Nov 91 09:28:27 MST From: Al Stavely Message-Id: <9111071628.AA02989@jupiter.nmt.edu> To: Jonathan.Bowen@prg Subject: Re: Software safety, formal methods and standards In-Reply-To: <2464@culhua.prg.ox.ac.uk> Organization: New Mexico Tech, USA This was posted some time ago. I haven't been able to find descriptions of the standards mentioned in any literature available to me -- if you find any, I'd like to hear about them! ------------------------------ >From: Chris.Holt@newcastle.ac.uk (Chris Holt) >Newsgroups: comp.software-eng >Subject: Re: Formal Specifications Required? >Message-ID: <1991Sep25.175728.11714@newcastle.ac.uk> >Date: 25 Sep 91 17:57:28 GMT > >iainw@bmdhh260.tmc.edu (Iain Woolf) writes: >>In article <1991Sep23.184437.27898@ennews.eas.asu.edu> collier@enuxha.eas.asu.edu (Ken Collier) writes: >>> >>>I recently heard an unsubstantiated rumor that Britain is requiring that >>>formal methods be used in the specification of all software developed for use >>>by its government agencies. Can anyone substantiate (clarify, etc.) or refute >>>this rumor. It seems to me that it has some very interesting and serious >>>ramifications. Anyone? > >>Most work done for Government and MOD will only be contracted to companies >>who have BS5750 - whether this is official or just an official (or even >>unofficial) recommendation, I don't know. > >Also, 0055 and 0056 look as though they'll want some pretty >heavy formal methods (though there is a clause that "rigorous >argument" will be good enough, whatever that means). > > Chris.Holt@newcastle.ac.uk Computing Lab, U of Newcastle upon Tyne, UK > "Where lies the land to which the ship would go? Far, far ahead..." - AHC -- - Allan Stavely, New Mexico Tech, USA >From rushby@com.sri.csl Sun Nov 10 01:11:01 1991 Sun, 10 Nov 1991 01:10:26 +0000 Date: Sat 9 Nov 91 11:28:18-PST From: John Rushby Subject: Safety standards To: Jonathan.Bowen@prg Cc: RUSHBY@com.sri.csl Message-Id: <689714898.0.RUSHBY@csl.sri.com> Mail-System-Version: Sender: rushby@com.sri.csl Jonathan, Two other standards you might want to check out are a recent draft Canadian standard for safety-critical Nuclear (powerstation) systems drawn up by David Parnas. I have a copy of that somewhere. The other, and by far the most important, is the revision to DO178A (to be called DO178B), which is the standard governing computerized control systems in (US) commercial aircraft. There is nothing published on this, and the discussion process is on-going, so you'll need to talk to an insider to find out what's up. Mike DeWalt (FAA) and Jim McWha (chief of flight controls for the 777--next big Boeing: FBW twin) will be at Sigsoft91, so that would be a good excuse for attending. John ------------------------------ >From parnas@ca.mcmaster.eng.qusunt Tue Nov 12 22:19:47 1991 Date: Tue, 12 Nov 91 09:41:55 EST From: David Parnas Subject: Re: Software safety, formal methods and standards To: Jonathan.Bowen@prg Message-Id: <9111121441.AA12096@qusunt.eng.mcmaster.ca> ... The AECB draft standard can only be obtained from the AECB. You might write to Dr. Kurt Asmis. His email is ASMISGK@NVE.CRL.AECL.CA Prof. David Lorge Parnas Communications Research Laboratory Department of Electrical and Computer Engineering McMaster University, Hamilton, Ontario Canada L8S 4K1 Telephone: 416 525 9140 Ext. 7353 Telefax: 416 521 2922 email: parnas@sscvax.cis.mcmaster.ca >From leveson@cs.washington.edu Tue Nov 12 22:25:23 1991 Message-Id: <9111111855.AA19513@whalespout.cs.washington.edu> To: Jim Horning Cc: Jonathan.Bowen@prg Subject: Re: I'll bet RISKS readers could help here... In-Reply-To: Your message of "Mon, 11 Nov 91 10:34:35 -0800." Date: Mon, 11 Nov 91 10:55:15 -0800 From: leveson@edu.washington.cs I was involved with DO178B in the beginning, i.e., attended some meetings and wrote some minority views up (I was usually in the minority :-)). However, I got busy with TCAS and attending all those meetings and have not had time to participate. Frankly, I think the whole aircraft certification attitude toward safety is pretty bad -- but historically the commercial aircraft industry has never been interested in much of anything other than reliability. I am currently writing a book on system/software safety while on sabbatical and will be including a chapter (and maybe more) on regulation and standards issues. Personally I find them very dangerous and try to stay away from them. Ethically such efforts bother me as they tend to be used by manufacturers to limit their liability and their own efforts. This is particularly true with DO178A and B. Standards that specify exactly what a manufacturer must do also provide them with a list of things that they will do and no more. And how well they do even the things specified are usually not included. I much prefer standards that tell manufacturers what their goals should be and then provide mechanisms to approve their plans, procedures, and success. In general, I believe that standards that take away responsibility and accountability from the manufacturer will lead to decreased safety. Specifying particular techniques to use take away that responsibility and accountability. nancy >From martinc%edu.unc.cs@org.mcnc.mcnc Wed Nov 13 02:49:02 1991 Date: Mon, 11 Nov 91 11:44:26 -0500 From: "Charles R. Martin" Message-Id: <9111111644.AA04223@grover.cs.unc.edu> To: Jonathan.Bowen@prg In-Reply-To: <9111071410.AA16469@topaz.comlab.ox.ac.uk> Subject: Re: Software safety, formal methods and standards Sender: martinc%edu.unc.cs@org.mcnc.mcnc Jonathan.Bowen@prg.oxford.ac.uk writes: > Charles, > > Thanks for the contacts. I've read quite a lot of Nancy Leveson's papers > (and know that she is a leading light in this area). What is John McHugh's > contribution to the field? > He has been dealing with safety to some extent as part of a more general definition of trust; he's also been doing a safety tutorial. I'm not keeping up with him on that, because we've been working together on security modeling stuff, but I know he's doing some. ... >From Debra_Sparkman.ADD%gov.llnl.ocf.lccmail@gov.llnl.ocf.ocfmail Thu Nov 14 05:19:18 1991 Message-Id: <9111122048.AA06987@ocfmail.ocf.llnl.gov> Date: 12 Nov 91 12:48:32 From: Debra Sparkman Subject: Software Safety, Formal Met To: Jonathan.Bowen@prg Cc: Debra_Sparkman.ADD@gov.llnl.ocf.lccmail Sender: Debra_Sparkman.ADD%gov.llnl.ocf.lccmail@gov.llnl.ocf.ocfmail Subject: Time:12:31 PM OFFICE MEMO Software Safety, Formal Methods,_ Date:11/12/91 Jonathan, My project is also reviewing standards and the state-of-the-practice in software safety, reliability, formal methods and life cycle processes as part of larger project. Your list seemed almost identical to mine. However, I have ISO 8807 a standard dealing with the formal method LOTOS. If you are interested the complete title is: "Information processing systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour". ... I've also attached a list of articles and publications I have (or am getting) on software safety and formal methods. I appologize for the format I dumped it from a database and the field separators didn't stay. If you cannot find what them please let me know I will send them to you. ... Debra Sparkman Lawrence Livermore National Laboratory P. O. Box 808 L-307 Livermore, CA 94550 USA Tele: (510) 422-1855 FAX: (510) 422-3194 Author Title Issued Issue or Publisher Bennett Forwards to safety standards Mar 1991 Software Eng. Journal Bjorner, Jones Formal Specification & Software Development 1984 Prentice-Hall Bjorner, Jones VDM - A Formal Method at Work - Experience with VDM in Norsk Data Mar 1987 Springer-Verlag Clements, Parnas A Rational Design Process: How And Why To Fake It Feb 1986 IEEE Trans. on Software Engineering Craigen FM89: Assessment of Formal Methods for Trustworthy Computer Systems 1990 Proceedings of the 12th International Conference on Software Engineering Craigen Tool Support for Formal Methods 1991 IEEE Craigen, Ryan FM91: Formal Methods Workshop 1991 IEEE Craigen, Summerskill Formal Methods for Trustworthy Computer Systems - FM89 1990 Springer-Verlag Fraser, Kumar, Vaishnavi Informal and Formal Requirements Specification Languages: Bridging the Gap May 1991 IEEE Trans. on Software Engineering Gabrielian, Franklin Multilevel Specification of Real-Time Systems May 1991 Communications of the ACM Gerhart Applications of Formal Methods: Developing Virtuoso Software Sep 1990 IEEE Software Gerhart Formal Methods: An International Perspective 1991 IEEE Gerhart Preliminary Summary: FM89 Assessment of Formal Methods for Trustworthy Computer Systems Dec 1989 ACM SIGSOFT Gong, Wing Raw Code, Specification, and Proof of the Avalon Queue Example Aug 1989 Carnegie Mellon University - Computer Science #CMU-CS-89-172 Guttag, Horning Introduction to LCL, A Larch/C Interface Language Jul 1991 Digital Systems Research Center Guttag, Horning, Wing Larch in Five Easy Pieces Jul 1985 Techincal Report 5, DEC Systems Research Center Guttag, Horning, Wing The Larch Family of Specification Languages Sep 1985 IEEE Software Hall Seven Myths of Formal Methods Sep 1990 IEEE Software Harel Statecharts: A Visual Formalism for Complex Systems Aug 1987 Sciece of Computer Programming Heninger Specifying Software Requirements for Complex Systems: New Techniques and their Application Jan 1980 IEEE Trans. on Software Engineering Hill, Robinson, Stokes Safety-Critical Software in Control Systems Nov 1989 IEC Proceedings of Computers and Safety, Nov 8-10, 1989 Jones LM3: A Larch Interface Language for Modula-3, A Definition and Introduction, Version 1.0 Jun 1991 Digital Systems Research Center Jones Systematic Software Development Using VDM 1986 Prentice-Hall Jones, Bjorner Formal Specification & Software Development 1982 Prentice-Hall Lafontaine, Ledru, Schobbens An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study May 1991 Communications of the ACM Leveson Evaluation on Software Safety 1990 IEEE McDermid, Thewlis Safety-critical systems - Editorial Mar 1991 Software Eng. Journal Milner A Calculus of Communicating Systems 1986 Nix, Collins The Use of Software Engineering, Including the Z Notation, in Development of CICS 1988 Quality Assurance pg 102-110 O'Neill VDM development with Ada as the target language 1988 Lecture Notes in Computer Science Oneill, Clutterbuck, Farrow, Summers, Dolman The Formal Verfication of Safety-Critical Assembly Code 1988 Proceedings of IFAC SAFECOMP Conference, Pergammon Press Parnas, Clements, Weiss The Modular Structure of Complex Systems Mar 1984 Proceedings on the Seventh International Conference on Software Engineering/IEEE Trans. on Software Engineering Mar 1985 Pedersen, Klein Using the Vienna Development Method (VDM) To Formalize a Communication Protocol Nov 1988 Carnegie-Mellon/Software Engineering Institute/Defense Technical Information Center Rollins, WIng Specifications as Search Keys for Software Libraries Jun 1990 Proceedings of the International Conference on Logic Programming - Paris, FranceSpivey Introducting Z: A Specification Language and is Formal Semantics 1988 Cambridge University Press Spivey The Z Notation: A Reference Manaul 1987 Prentice Hall Turner, various Formal Description Techniques 1989 North-Holland, Amsterdam unknown Software Safety: Two Approaches unknown via Dennis Lawrence various Formal Description Techniques-Proceedings for the First International Conference on FDT Sep 1988 North-Holland Wing A Larch Specification of the Library Problem Dec 1986 Carnegie Mellon University - Computer Science #CMU-CS-86-168 Wing A specifier's introduction to formal methods Sep 1990 IEEE Computer Wing Specifying Avalon Objects in Larch Dec 1988 Carnegie Mellon University - Computer Science #CMU-CS-88-208 Wing Using Larch to Specify Avalon/C++ Objects Sep 1990 IEEE Transactions on Software Engineering Wing Writing Larch Interface Language Specifications Jan 1987 ACM Transactions on Programming Languages and Systems Wing, Gong Experience with the Larch Prover Sep 1989 Jeannette Wing IEE Proceedings of Computers and Safety, Nov 8-10, 1989 Nov 1989 >From jpyra@ca.ns.nstn.fox Thu Nov 14 22:03:15 1991 Thu, 14 Nov 1991 20:42:41 +0000 Thu, 14 Nov 91 12:13:33 AST Date: Thu, 14 Nov 91 12:11:56 EST From: (Jim Pyra) jpyra Message-Id: <43934.jpyra@fox.nstn.ns.ca> To: Jonathan.Bowen@prg Subject: Safety Standards Jonathan: You may be interested in the proposed standard for "SOFTWARE FOR COMPUTERS IN THE SAFETY SYSTEMS OF NUCLEAR POWER STATIONS" based on IEC Standard 880 for the Atomic Energy Control Board of Canada and written by Dr. David Parnas. You can reach Dave Parnas at Helpful Jim Standard disclaimers... Jim Pyra email:jpyra@fox.nstn.ns.ca PRIOR Data Sciences Ltd. Phone:(902)423-1331 5475 Spring Garden Rd., Suite 601 FAX: (902)425-3664 Halifax N.S. B3J 3T2 Canada >From heiner%b11.dnet%uucp.b21@de.uni-dortmund.informatik.unido Fri Nov 15 14:03:48 1991 From: heiner Message-Id: <9111151335.AA11127@unido.informatik.uni-dortmund.de> Date: Fri, 15 Nov 91 14:10:07 +0100 To: "unido!Jonathan.Bowen@comlab.ox.ac.uk"@dnet.B21 Sender: "b11.dnet!heiner" Subject: Your request for software safety related standards via Risks Forum Dear Mr. Bowen, there are some more standards or draft standards regarding that subject we know of, but they are rather general and not oriented towards formal methods: "Software for computers in the safety system of nuclear power stations"; IEC 45A(Central Office)88, 1984. Comment: The scope of this standard is much broader than the title suggests. The rules of this standard have been derived from preliminary guidelines produced by the European Workshop on Industrial Computer Systems (EWICS) TC7. As you probably know these guidelines have been edited in three volumes "Dependability of Critical Computer Systems" by Felix Redmill, Elsevier Applied Science, since 1988. EWICS TC7 is still active. The chairman is Robin Bloomfield with Adelard in London, phone: 081 983 1708. There is a subgroup on formal methods which is chaired by Robin Bloomfield too, I think. "Software Considerations in Airborne Systems and Equipment Certification"; RTCA/DO-178A, March 1985. Comment: This is a guideline being widely applied in civil aviation. "Principles for computers in safety-related systems"; preliminary standard DIN VDE 0801, January 1990. Comment: Though preliminary this standard is actually the most important non-application-specific standard in Germany for safety related systems. Its english translation has been submitted to IEC. I would be glad if I could help you a little bit, and I would be even gladder if you would send me your review paper. Please don't hesitate to mail again if you need more information (but please don't use the reply-mechanism; we often got problems receiving replies.) Best regards Guenter Heiner Systems and Software Technology Research Daimler-Benz AG Alt-Moabit 91b D-1000 Berlin 21 phone: ++49-30-39982237 fax: -39982107 email: heiner@b21.uucp unido!b21!heiner >From JZ01%swt.decnet%net.the.relay@net.the.nic Sat Nov 23 22:54:44 1991 Date: Sat, 23 Nov 1991 09:44 CST From: JZ01 Subject: Re: Software safety, formal methods and standards To: jonathan.bowen@prg Message-Id: <01A8C0F6B0201E41@nic.the.net> Sender: JZ01 Jon, I think you have to look into the work of EWICS (European Workshop on Industrial Computer Systems), TC7 on Realiability and Safety. The related publications are: * Felix Redmill (Ed.), Dependability of Critical Computer Systems, Volumes I and II, Elsevier Applied Science, London, 1988 and 1989 (Crown House, Linton Road, Barking, Essex, IG11 8JU) * A huge number of Working Papers, some of the related to your topic. To get the Working Papers you may contact the current Chairman, Robin Bloomfield, of Adelard, of the former Chairman, Barry Daniels, of NCC, Manchester. Robin Bloomfield EWICS Chairman Adelard 28, Rhondda Grove London E3 5AP Phone: 44-0-13187579 Fax: 44-0-18524738 Since safety is directly related to reliability, you may also try the following two items: * A Specification Language for Reliable Real-Time Systems, pp. 273-289, by H. Wupper, J. Vytopil, in J.Zalewski, W.Ehrenberger, Hardware and Software for Real-Time Process Control, North-Holland, 1989 The same book contains three papers on safety, one of them titled "THe Impact of Standardization on Software Quality, Systems Safety and Reliability". ISBN 0-444-87127-6 * Study of the Feasibility of Using a Formalized Language for the Description of reliability Problems, N.D. Deans, A.J. Miller. Report EUR 11753EN, Comm. of the European Communities, 1988 I got it from Tony Miller, who is with Robert Gordon's Institute of Technology at Aberdeen, Scotland. Of course, I have the above book in my office, too, so if you'll have problems with finding it, let me know. Please also note that I would be interested in getting a copy of your paper. I may also review it before publication, if it makes any sense to you. Regards, Janusz Zalewski Dept. of Computer Science Southwest Texas State University San Marcos, TX 78666-4616 E-mail: JZ01@SWTEXAS.Bitnet Phone: 512-245-3873 Fax: 512-245-3040 ------------------------------ End of RISKS-FORUM Digest 12.BOWEN ************************