Issue No. 09 - Sept. (1986 vol. 12)
Robin E. Bloomfield , Department of Scientific Services, Central Electricity Generating Board, Gravesend, Kent DA 12 2RS, England
Peter K. D. Froome , Department of Scientific Services, Central Electricity Generating Board, Gravesend, Kent DA 12 2RS, England
The increasing use of computers to protect or control potentially hazardous processes leads to a need for effective methods to assess the software they execute. This correspondence presents a case study in which the Vienna development method (VDM), a formal specification and development methodology, was used during the analysis phase of the assessment of a prototype nuclear reactor protection system. The VDM specification was also translated into the logic language Prolog to animate the specification and to provide a diverse implementation for use in back-to-back testing. The authors claim that this technique provides a visible and effective method of analysis which is superior to the informal alternatives.
History, Animation, Software, Formal specifications, Abstracts, Data structures, Prototypes
R. E. Bloomfield and P. K. Froome, "The application of formal methods to the assessment of high integrity software," in IEEE Transactions on Software Engineering, vol. 12, no. , pp. 988-993, 1986.