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

The VDM [ 10 ] tool was used for specifying the whole system, which specified con-
current system behaviours. At the product design level, the VDM code was refined
into more concrete specifications, and a lower level code was formally specified and
developed using CCS [ 85 ]. The productivity of the system was better than the tra-
ditional system development and the quality of the system was improved through
finding some faults.
2.10.3 The Paris Métro Signalling System (SACEM)
The SACEM system [ 44 ] was developed by several industrial partners GEC Al-
sthom, MATRA Transport and CSEE (Compagnie des Signaux et d'Entreprises
Électriques) in 1989. The system was responsible for controlling the RER commuter
train system Paris. The existing system was made of embedded software and hard-
ware, where software had 21000 lines of code. Some parts of the SACEM software
were formally specified in the B modelling language [ 2 ] for the proving purpose.
The SACEM project is an example of “reverse engineering” process, where formal
specification and verification were conducted after developing the code. Finally, the
system was certified by the French railway authority.
ClearSy has developed the screen door controllers for Paris metro line using B
formal methods [ 71 ]. The models are developed using correct by construction ap-
proach and to prove the absence of failure in the system behaviour. A constructive
process was used during system specification and design leads to a high-quality
system.
2.10.4 The Traffic Collision Avoidance System (TCAS)
Formal specification of the Traffic Collision Avoidance System (TCAS) [ 15 ]is
another interesting example of the application of formal methods in the air-traffic
transport domain. The TCAS system is used by all commercial aircraft for reducing
the chance of a mid-air collision. In early 1990s, a safety critical system research
group at the University of California, produced a formal requirements specifica-
tion for the TCAS due to occurring some flaws in the original TCAS specification.
The formal specification was developed into Requirements State Machine Language
(RSML) [ 75 ], which is based on a variant of Statecharts [ 40 ]. The original specifi-
cation was not supported by existing formal methods tools, but nevertheless, it was
very useful for the project reviewers, in the sense of improving the original specifi-
cation. Heimdahl et al. [ 43 ] successfully checked the consistency and completeness
of the TCAS specification and provably-correct code generated from the RSML
specification.