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:
- The INMOS Transputer, which used FM for the floating-point unit and virtual channel processor.
- The Tektronix oscilloscope.
- The "Structured System Analysis and Design Method" toolset developed by Praxis.
- IBM's legendary CICS respecification.
- 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:
- The LaCoS (Large Correct Systems) project, which mades a toolset for a variant of VDM with the explicit goal of technology transfer.
- The TBACS (Token-based Access Control System) smartcard system.
- 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.
You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.