Investigating the Influence of Formal Methods

Formal methods promise much, but can they deliver? In this project, results are inconclusive, but careful data gathering and analysis helped establish influences on product quality. Practitioners and researchers continue to seek methods and tools for improving software development processes and products. Candidate technologies promise increased productivity, better quality, lower cost, or enhanced customer satisfaction. But we must test these methods and tools empirically and rigorously to determine any significant, quantifiable improvement. We tend to consider evaluation only after using the technology, which makes careful, quantitative analysis difficult if not impossible. However, when an evaluation is designed as part of overall project planning, and then carried out as software development progresses, the result can be a rich record of a tool's or technique's effectiveness. In this study, we investigated the effects of using formal methods to develop an air-traffic-control information system. Because we are studying one project in isolation, we cannot draw conclusions about the suitability of formal methods for all projects. As we describe in the sidebar "Can Formal Methods Always Deliver?" the jury is still out on when and whether formal methods improve products. Nevertheless, the lessons we learned are instructive, not only in showing how formal methods influenced code quality on this project, but also in highlighting the limitations of retrospective studies and their use in planning follow-up investigations. We describe what we did, as well as what we could have done had the study been carried out as the software system was being developed and tested. We also show how this preliminary investigation helps to suggest hypotheses for further studies. Thus, the lessons we learned can be applied not only to gauge the effects of formal methods but also in planning similar studies of other techniques and tools. The procedure we used was not predetermined; the results of one analysis step largely determined where we went next. Indeed, research often involves following one trail and then another, uncovering relationships and unearthing facts, until the picture begins to make sense. However, we did learn many specific lessons, which we hope will enrich future investigations.