Applying Formal Methods to a Telecommunications System in a Commercial Setting by Andre Wong and Marsha Chechik ABSTRACT Formal methods have long been advocated by the software engineering research community; however, most successful applications of formal methods are confined to safety-critical projects where software correctness is the pivotal goal. In contrast, the software industry seeks practical techniques that can be seamlessly integrated into their existing processes and improve productivity; absolute quality is often a desirable but not crucial objective. A number of formal methods have been designed to address this issue, and some have industrial-strength implementations that can be used effectively in a commercial setting. This paper describes a case study conducted in collaboration with Nortel to demonstrate the feasibility of applying formal methods to telecommunications systems. A lightweight formal method, SDL, was chosen by our qualitative CASE tool evaluation to model a multimedia-messaging system described by an 80-page natural language specification. Our model was used to identify errors in the software requirements document and to derive test suites, shadowing the existing development process and keeping track of a variety of productivity data. Creating a model which was easy to review by Nortel engineers, allowed us to locate specification errors that were missed by several manual inspections. In addition, the model was used to derive a variety of test cases that doubled the number of errors discovered by Nortel testers. The success of our case study was in finding a suitable project where we were able to integrate a well-chosen formal method into the existing development process.