Evaluating the effect of a lightweight formal technique in industry

We evaluate the effect of applying the commercial formal technique Analytical Software Design (ASD) to an industrial project. In ASD, interfaces and software designs are modelled using a formal tabular notation. The ASD tool set supports formal checks of these models, such as deadlock freedom and interface compliance. In addition, full code can be generated from design models. ASD has been applied at Philips Healthcare to develop parts of the software of interventional X-ray systems. We report about the experiences with the embedding of ASD into the development processes. The quality of the resulting code and the productivity has been analysed and compared to code developed with other techniques. We observe that the use of ASD leads to a strong reduction of the number of defects and an increase in productivity. The results are also compared to the literature about standards and related projects at other companies.