Experience report on developing the Front-end Client unit under the control of formal methods

Formal methods are extensively being applied to the development of control software units, of highly sophisticated X-ray machines, at Philips Healthcare. One of the early units incorporating formal methods is the Front-end client (FEClient), which was developed under the control of formal technologies, supported by the Analytical Software Design (ASD) method. As a result, only eleven coding errors were detected during the construction of 28 thousands lines of code. Team members attribute the ultimate quality of the software to the rigor of the formal technologies supplied by the ASD method. In this paper we report about the experience of applying ASD to the development of the FEClient, and we show how formal methods substantially enhanced its quality. We also discuss the nature of the errors found during the construction of the unit