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

Electronic Purse [ 16 , 100 , 112 ] is an electronic system for e-commerce, based on
smart card, produced by NatWest Development Team. Electronic purse must ensure
the security of each transaction. Formal methods were used by a several group of
researchers for verifying the protocol of money transfer over an insecure and lossy
medium. The whole formal specification of the Mondex system was developed and
proved from an abstract model to concrete model using refinement approach. The
abstract model was focused specially on the safety properties of the system.
2.10.9 Darlington: Trip Computer Software
This case study describes the computerised shutdown system of Darlington Nuclear
Generating Station (DNGS). The shutdown application contains two independent
systems, Shutdown System One (SDS1) and Shutdown System Two (SDS2). The
SDS1 is operated by dropping neutron-absorbing rods into the core; the SDS2 is
operated by liquid poison injection into the moderator [ 25 , 107 ]. The Trip comput-
ers are connected with plant sensor to shutdown the system, whenever shutdown is
required. This Trip computers are used alone to concern the safety issues. The shut-
down systems were required a high level of confidence to obtain the certification
standard. The regulatory bodies were not sure to check the validity of the software.
Thus, the formal techniques were used to identify the discrepancies in the shutdown
systems. The verification process was conducted on the complete system. The entire
process is reported in [ 5 ]. The final system was redesigned or modified according to
the regulators and concludes that the new develop system is safe for use.
2.10.10 The BOS Control System
The BOS Software is an automatic system, which is used to protect the harbour
of Rotterdam from flooding, while concurrently also controls the ship traffic [ 104 ].
BOS controls a movable barrier, taking decisions of when and how the barrier has to
move, based on chaotic behaviour of water level, tidal info, and weather precondi-
tions. BOS is a highly critical system, which is characterised by IEC 61508 [ 53 ]. The
design and implementation of the BOS were undertaken by CMG Den Haag B.V., in
collaboration with a formal methods team at University of Twente. Different kinds
of methodologies were applied during development of the system. Mainly formal
methods were used to specify the crucial part of the system for validating the system
specification. The control part of the system was formally specified in PROMELA
and the data part into Z specification language. The formal validation of the design
focused on the communication protocol between BOS and an environment. The fi-
nal implementation of the system was done in C++ which was generated from Z
specification. At the initial level of the system development, formal methods helped
to uncover several issues in the existing system. Overall use of the formal methods
improves the quality of the system.