AN INVITATION TO FORMAL METHODS

One of the most challenging tasks in software system design is to assu re reliability, especially as these systems are increasingly used in s ensitive and often life-critical environments such as medical systems, air traffic control, and space applications. It is therefore essentia l for developers to employ those methods that offer a high degree of a ssurance that the system's requirements accurately capture the users' critical requirements and that an implementation in software (or hardw are) is an accurate realization of the design. Software reliability, a lthough the primary concern of the computing industry, is not the only one. Another major concern has been the increased cost of developing and maintaining software. Precise, up-to-date figures representing the actual cost of software in industry are neither available nor easy to establish. Boehm suggested that the worldwide cost of software in 198 5 was roughly $140 billion ($70 billion in the US alone).(1) Even if w e assume a modest growth rate of 10 percent per year (Boehm suggested 12), the software cost in the year 2000 will be close to $600 billion ($300 billion in the US). Much of software's cost stems from testing a nd maintenance. The absence of rigorous practices that eliminate resid ual specification and design errors (caused by imprecision, ambiguity, and sometimes, plain mistakes) has translated into a significant port ion of this cost. Many claim that formal methods not only provide adde d reliability but also have the potential to reduce costs. They provid e a notation for the formal specification of a system whereby the desi red properties are described in a way that can be reasoned about, eith er formally in mathematics or informally but rigorously. In essence, f ormal methods offer the same advantages for software (or even hardware ) design that many other engineering disciplines have exploited-namely , mathematical analysis using a mathematically based model. Such model s allow the designer to predicate the behavior and validate the accura cy of a system instead of having to rely entirely on nonassuring exhau stive testing. The clear advantages of a more mathematical approach to software design has certainly been well documented; the literature co ntains many excellent examples of applications of formal methods for l arge, critical, or even business transaction systems. Despite the evid ence, however, a large percentage of practitioners see formal methods as irrelevant to their daily work. To be sure, practitioners can't sim ply be blamed for their skepticism. What is hindering the adoption of formal methods by industry? Is the notation too complex? Or are existi ng formal methods unable to contribute to, benefit from, or be integra ted with traditional methodologies? Is there still a perception of hig h complexity and costs? Has the barrier been the lack of easy-to-use s upport tools? Or would an increase of formalism in computer science or software engineering education translate into a more formal approach in industry by the next generation of software engineers? In seeking a nswers to these questions, I contacted some of the best minds in acade mia and industry, asking them to share their insights.