Application of formal methods to testing of industrial-size systems.

This work is a collaboration with Nortel Toronto, in which we aim to demonstrate applicability and financial feasibility of formally specifying telephony software. In particular, we are interested in using this formal model to aid in testing. Our goals are 1) to identify a suitable project for which a formal method can be effectively applied; 2) to select a suitable formal method that would support testting; 3) to specify a portion of the existing Nortel system; 4) to use the model to generate teset cases; 5) to evaluate results.

The first phase of the project is completed and described in a paper Applying Formal Methods to a Telecommunications System in a Commercial Setting to appear in 11th International Conference on Software Engineering and Its Applications, December 1998, Paris, France.

The second phase requires a formal evaluation of the work. To do so, we are

• conducting a number of interviews with Nortel developers and testers
• conducting a one-day workshop on SDL - the method we chose for the study
• setting up and evaluating two experiments on effectiveness of using SDL for modeling and testcase generation.

From the UofT side, this project is being undertaken by A. Wong and M. Chechik.