Software metrics are widely used to measure the quality of software and to give an early indication of the efficiency of the development process in industry. There are many well-established frameworks for measuring the quality of source code through metrics, but limited attention has been paid to the quality of software models. In this article, we evaluate the quality of state machine models specified using the Analytical Software Design (ASD) tooling. We discuss how we applied a number of metrics to ASD models in an industrial setting and report about results and lessons learned while collecting these metrics. Furthermore, we recommend some quality limits for each metric and validate them on models developed in a number of industrial projects.

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.

During the last two decades, we modelled the behaviour of a large number of systems. We noted that different styles of modelling had quite an effect on the size of the state spaces of the modelled systems. The differences were so substantial that some specification styles led to far too many states to verify the correctness of the model, whereas with other styles, the number of states was so small that verification was a straightforward activity. In this article, we summarize our experience by providing seven specification guidelines to keep state spaces small. For each guideline, we provide an application, generally from the realm of traffic light controllers, for which we provide a ‘bad’ model with a large state space, and a ‘good’ model with a small state space. The good and bad models are both suitable for their purpose but are not behaviourally equivalent. For all guidelines, we discuss circumstances under which it is reasonable to apply the guidelines. Copyright © 2014 John Wiley & Sons, Ltd.

This paper reports on the steps to formally specify and verify the behavior of a controller of a power distribution unit (PDU) using the Analytical Software Design (ASD) method. The controller of the underlying PDU mainly controls the distribution of power and network messages to a number of attached PCs and devices of X-ray systems. The behavioral correctness of the controller is critical in order to provide the clinical users the expected behavior of the system. The design of the controller was thoroughly reviewed by team members but, as a result of the behavioral verification using ASD, two previously unrevealed errors were identified within the design of the PDU controller. According to the development team of the PDU the work has had a major benefit of improving the design of the controller and locating errors that would have been hard to find otherwise by traditional testing.

Formal methods are being applied to the development of software of various applications at Philips Healthcare. In particular, the Analytical Software Design (ASD) method is being used as a formal technology for developing defect-free control software of highly sophisticated X-ray equipments. In this paper we analyze the effects of applying ASD to the development of various control software units developed for the X-ray machines. We compare the quality of these units with other units developed in traditional development methods. The results indicate that applying ASD as a formal technology for developing control software could result in fewer defects.