Today I started looking over An International Survey of Industrial Applications of Formal Methods, a study of 12 formal methods projects sponsored by the US Dept. of Commerce, among others, and published in 1993 (available here). I got through the first 23 pages (of the PostScript file) of Volume 1: Purpose, Approach, Analysis, and Conclusions.
So far, it's mostly just summary. I've read about this paper before, so I've yet to find any revelations. I did see the summaries of the 12 case studies, though. They were divided into three categories: regularotry, commercial, and exploratory. The project breakdown goes as follows:
- Darlington Nuclear Generator Station (DNGS): Post-hoc verification of the software shutdown system using the Software Cost Reduction approach in order to get a license to operate.
- Multinet Gateway System (MGS): A security-sensitive internet gateway project that used the Gypsy Verification Environment.
- SACEM: Also known as the Paris metro project to increase "person-flow" by having less time between trains. Used B and Hoare Logic to help meet safety requirements.
- Traffic Alert and Collision Avoidance System (TCAS): The title says it all - a system to keep planes from hitting each other. The summary didn't say much, but I believe from other reading that this may have been one of Praxis's projects.[/numlist]Commercial projects
- Structured Systems Analysis and Design Method Toolset: A project by Praxis to build tools to support this design method, using a Z specification.
- Customer Information Control System (CICS): a trnasaction processing system that IBM partially redesigned using Z. From other reading, there is apparently there is some disagreement over exactly how successful this project was.
- Cleanroom Software Methodology: A pair of projects for NASA and IBM. These are a system for ground control of satelites and a system to convert COBOL systems into a "structured programming equivalent."
- Tektronix Oscilloscope: An oscilloscope project using Z.
- INMOS Transputer: INMOS used Z, Occam, Communicating Sequential Processes, and the Calculus of Communicating Systems to design their Transputer family of VLSI circuits.[/numlist]Exploratory projects
- Large Correct Systems (LaCoS): A technology transfer project involving the Rigorous Approach to Industrial Software Engineering (RAISE), a variant of VDM.
- Token-based Access Control System (TBACS): A prototype smart card system for network access that used theorem proving.
- Hewlett-Packard Medical Instruments: A real-time medical database that was developed using a variant of VDM. Was considered a failure because time to market was the key feature.