Formalizing requirements in a commercial setting: A case study

Formal description techniques (FDTs) have long been advocated as a solution to problems posed by requirements specified in natural language; however, successful applications of FDTs have been confined mostly to safety-critical projects.;This thesis describes a research project conducted in collaboration with Nortel to investigate the technical and the economic feasibility of applying FDTs in a commercial setting. By first interviewing the Nortel engineers, we identified problems with their development process and proposed criteria for our quantitative formal description method evaluation. We selected a method that was suitable to our project and usable in the Nortel environment and applied it to a multimedia-messaging subsystem; the resulting model was used to identify requirements errors and to derive test suites, shadowing the existing development process and keeping track of a variety of productivity data. By amortizing the cost of formalization to the testing phase, we showed that the use of FDTs could increase the quality of the software without lengthening the development cycle.