Specification and Validation of Telecommunications Systems
with Use Case Maps and Lotos

by Daniel Amyot

Thesis Submitted in Partial Fulfillment of the Requirements for the
Degree of Doctor of Philosophy in Computer Science under the auspices of
the Ottawa-Carleton Institute of Computer Science School of Information
Technology and Engineering (SITE),

University of Ottawa,
Ottawa, Ontario, Canada
September 2001


Abstract

The functional modeling of telecommunications systems requires an early
emphasis on behavioral aspects. In the first stages of common development
processes, telecommunications features, services, and functionalities
are defined in terms of informal requirements and visual descriptions. As
these descriptions grow and evolve, they quickly become error-prone and
difficult to understand. Consequently, designs can hardly be checked or
validated against such descriptions.

This thesis proposes an innovative methodology named
Specification-Validation Approach with LOTOS and UCMs (SPEC-VALUE),
which tackles these problems using two notations. The first notation,
called Use Case Maps (UCMs), is used to capture and integrate functional
requirements in terms of causal scenarios. Scenarios describing system
views, uses, and services are becoming a common method of capturing
functional requirements of reactive and distributed systems. They are
particularly appropriate to represent behavioral aspects so that various
stakeholders can understand them.  In addition to these general properties
of scenarios, UCMs can help reasoning about system-wide functionalities
at a high level of abstraction. Integrating UCMs together also helps
avoiding many undesirable interactions, usually resulting from the
composition of different scenarios, before the generation of prototypes.

The second notation is the formal specification language LOTOS. It
will be shown that UCM scenarios bound to architectural components can
be translated into high-level LOTOS specifications.  In turn, these
specifications can be used as prototypes to animate UCMs and to validate
high-level designs against requirements systematically through numerous
techniques, including functional testing based on UCMs. LOTOS possesses
powerful testing concepts and tools that excel at detecting errors and
undesirable interactions. LOTOS represents a judicious formalism here
because it supports many UCM constructs directly, and it complements
most of UCMs weak areas related to the analysis of systems.

SPEC-VALUE introduces theories and techniques for constructing LOTOS
specifications from UCMs, for deriving validation test cases from
UCMs, and for measuring the structural coverage of LOTOS specifications
achieved during validation. An ongoing example is used to illustrate these
concepts: the Tiny Telephony System. The thesis validates the SPEC-VALUE
methodology through its application to various telecommunications
systems (Group Communication Server, Group-Call service of GPRS, feature
interactions, agent-based simplified basic call, and GSMs MAP protocol),
and concludes with an assessment of these experimental results.