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.