Formal Modeling in a Commercial Setting: A Case Study

TL;DR

This case study demonstrates how formal modeling with SDL can identify errors and generate test suites in telecommunication system development, improving accuracy and productivity tracking.

Contribution

It shows the practical application of formal modeling techniques in a commercial telecommunication setting, including error detection and test case derivation.

Findings

Error detection in requirements document

Generation of test suites from formal models

Enhanced productivity tracking

Abstract

This paper describes a case study conducted in collaboration with Nortel to demonstrate the feasibility of applying formal modeling techniques to telecommunication systems. A formal description language, 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.