Background - Using Event-B for Critical Device Software Systems - page 33

2.10.5 The Rockwell AAMP5 Microprocessor
The microcode of AAMP5 microprocessor was formally specified and verified,
which was produced by Rockwell [ 84 ]. This project was undertaken by Collins
Commercial Avionics (CCA) and SRI. The AAMP5 microprocessor has a complex
architecture, designed for Ada language and implements floating-point arithmetic in
the microcode. PVS theorem prover [ 26 ] was used for specifying and verifying the
microcode of the AAMP5 instructions.
2.10.6 The VIPER Microprocessor
VIPER microprocessor was developed with a simple architecture, specifically for
the safety critical applications [ 27 ]. Formal methods were used throughout the de-
velopment cycle of VIPER, at the different level using different techniques. This
work was conducted by the Royal Signals and Radar Establishment (RSRE). Some
parts of the system were specified by the HOL theorem prover and LCF-LSM lan-
guage [ 37 ]. Mainly top level specification and abstract level view for register trans-
fer level were carried out in the HOL. There was not any significant result through
this formal verification except finding some minor flaws in the system, which had
no concerns for the fabricators of the chip.
2.10.7 INMOS Transputer
In 1985, a microprocessor manufacturing company INMOS starts to use the formal
program specification, transformation and proof techniques for designing a micro-
processor. Formal methods based techniques were used for designing or developing
the components of the INMOS Transputer. Different types of formal techniques
like, Z, Occam and CSP were the main tools for specifying system requirements.
For example, the Z specification language was used to specify the IEEE Floating
Point Standard, and the combined approach of Z and Occam was used to design the
scheduler, for the microprocessor. Later, the CSP with other formal techniques were
used in design and verification of new features on the third generation Transputer
(T9000), Virtual Channel Processor (VCP). The VCP is a device that allows several
logical connections between two processors that was implemented by a single phys-
ical connection. This successful application of formal methods offers to apply into
a hardware engineering environment [ 25 ].
2.10.8 The Mondex Electronic Purse
In this section, we have mentioned the Mondex Electronic Purse as a significant ex-
ample of the use of formal methods in an industrial-scale application. The Mondex