FM Thesis

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:

Regulatory projects

1. 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.
2. Multinet Gateway System (MGS): A security-sensitive internet gateway project that used the Gypsy Verification Environment.
3. 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.
4. 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.

Commercial projects

1. Structured Systems Analysis and Design Method Toolset: A project by Praxis to build tools to support this design method, using a Z specification.
2. 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.
3. 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."
4. Tektronix Oscilloscope: An oscilloscope project using Z.
5. INMOS Transputer: INMOS used Z, Occam, Communicating Sequential Processes, and the Calculus of Communicating Systems to design their Transputer family of VLSI circuits.

Exploratory projects

1. Large Correct Systems (LaCoS): A technology transfer project involving the Rigorous Approach to Industrial Software Engineering (RAISE), a variant of VDM.
2. Token-based Access Control System (TBACS): A prototype smart card system for network access that used theorem proving.
3. 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.