Phase Automaton for Requirements Scenarios

Bill MITCHELL, Robert THOMSON, and Clive JERVIS

Motorola UK Research Lab
Jays Close, Basingstoke, RG22 4PD, UK
{b.mitchell, brt007, clive.jervis}@motorola.com

Abstract. Requirements specifications for wireless telecommunications systems are often only partially defined, usually consisting of a set of normative scenarios together with scenarios for some of the more important exceptional behaviours. A major challenge is to find effective means of analysing such specifications formally in order to detect errors as early in the lifecycle as possible. The challenge arises because existing techniques generate too many bogus reports due to the incomplete nature of the specifications, so masking genuine errors, and generate too large a state space for effective analysis.

Motorola UK Research Lab has been collaborating with testing, architecture and design groups throughout Motorola to investigate this area over the last few years. We define a particular semantics for combining scenarios that can be conveniently represented by a new kind of automata, called phase automata. The semantics uses information embedded in the specification to factor the resulting automata into phases, which gives a more compact representation than other approaches, and concurs with engineering use. In this paper we assume scenarios are defined as MSCs, which is indeed standard practice in Motorola and other wireless telecommunications companies, though the results apply more generally than this.

An internal software tool, FATCAT, has been developed by Motorola UK Research Labs that constructs phase automaton representations for each instance from a set of normative MSCs, analyses them and, if any conflicts are found, outputs MSCs that describe the problem scenarios. FATCAT has been used to analyse features being developed for 3G handsets, where it has discovered errors in the specifications that had previously gone undetected and which were subsequently uncovered only during field testing of pre-release models. FATCAT is built on patented technology already developed by Motorola UK Labs for the ptk software tool. The ptk tool generates a set of conformance tests from a collection of MSCs. ptk has been developed over a number of years and is now used by engineering groups throughout Motorola.