FM Thesis

Well, I didn't get around to posting my day's progress on Wednesday, so I guess I'll be summarizing more than usual today. Unfortunately, I didn't get anything done yesterday night, as I had other things I needed to do.

Wednesday and today I got through some more of the IFM92 survey. I covered the commercial case cluster, the exploratory cluster, and the event and timing section.

The commercial cluster consisted of five projects:

1. The INMOS Transputer, which used FM for the floating-point unit and virtual channel processor.
2. The Tektronix oscilloscope.
3. The "Structured System Analysis and Design Method" toolset developed by Praxis.
4. IBM's legendary CICS respecification.
5. The "COBOL Structuring Facility" which used the Cleanroom method.

There are a few things to note here. First, the COBOL/Sf project was the only one that didn't use Z in some way. However, there were minor problems in that Z could not be used to model interfaces or real-time properties. Second, it seems that only INMOS attempted any sort of formal proof of correctness. Apparently this was not a big concern for the other organizations, although the formal specifications did at least help in generating test cases.

Overall, the results were not too surprising. FM were seen to have a generally good impact on the projects. Although only INMOS attempted verification, the CICS and Tektronix people apparently thought the formal specification gave them more "intellectual ownership" of the systems.

There was apparently no dramatic affect on the economic factors involved in most of the products. Although it seems that most saw improved quality (at least subjectively), there was no substantial difference between the cost of the project and the estimated time and cost to do it using conventional methods. The only exception was INMOS, who reported saving an estimated three months and three million pounds due to the FM reducing the amount of testing they needed to do. In terms of ongoing maintenance costs, there was little data collected. The only data point is COBOL/SF, which required one person/year for maintenance, which is less than would normally be expected. However, that might be due as much to the other aspects of Cleanroom as it is to FM.

There were three exploratory projects:

1. The LaCoS (Large Correct Systems) project, which mades a toolset for a variant of VDM with the explicit goal of technology transfer.
2. The TBACS (Token-based Access Control System) smartcard system.
3. The HP Medical Instruments case, which involved the creation of a VDM-based specification language with the goal of transferring FM technology to the rest of the organization.

To me, the results of this cluster seem less than stellar. All the groups learned a great deal from their respective projects, but there wasn't an awful lot of actual technology transfer. For instance, the LaCoS project, which seems to be the most successful, did transfer its work successfully to its partners, but it doesn't seem like they've done an awful lot with it.

The HP project didn't go so well. Apparently FM did not significantly increase the product's quality or time to market. Apparently management didn't see significant advantages to be gained and ended up disbanding the Fm groups.

The TBACS project seems to have had mixed results. The FM used did find a flaw in the prototype smartcard that would not have been detected by testing, and in that sense, were a success. However, other factors led the developers to decide against adopting them. Apparently they decided to file them away for use in future projects.

There weren't too many conclusions to be drawn in the event and timeline section. The common events seem to be the ones that introduced organizations to FM, i.e. the desire to try out new methods and the recognition of a serious problem that they could not solve with their current methods. There was not much commonality in timeframes or in events that kept them on the "formal methods path." However, with two exceptions (Tektronics and HP), all the organizations continue to use FM. Apparently Tektronix converted the Z specification to object-oriented code and decided to simply continue with that.

In other news, I also started reading up on Z a bit. I managed to get through the introductory chapter of Using Z: Specification, Refinement, and Proof tonight. Obviously I haven't gotten to the good part yet, so there's not much to say about it. However, I did see that the book includes a number of case studies that used Z, which may come in handy later.

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.