Formal Modeling and Test Generation Automation with Use Case Maps and LOTOS

by Leïla Charfi

Thesis submitted to the School of Information Technology and Engineering
in partial fulfillment of the requirements for the degree of Master of
Computer Science under the auspices of the Ottawa-Carleton Institute
for Computer Science

University of Ottawa
Ottawa, Ontario, Canada
March, 2001

Abstract

This thesis addresses the problem of formal modelling and test generation,
from system requirements represented in the form of Use Case Maps. In the
first part of our thesis, we present an existent development methodology
based on Use Case Maps for the design of the requirements and on LOTOS and
SDL for the formal modeling of telecommunication systems. We follow this
methodology for the formal specification and validation of a telephony
system using LOTOS. In the second part of the thesis, we develop a method
for the automatic generation of LOTOS scenarios from Use Case Maps called
Ucm2LotosTests. The obtained scenarios can be used for the verification
of the LOTOS specification built from the same Use Case Maps and for
conformance testing purposes at the implementation stage.  Finally, we
propose a development methodology based on Use Case Maps for the design of
the requirements and on LOTOS for the formal modeling of the system. In
addition, this methodology offers a fast test generation process; it
proposes the use of Ucm2LotosTests for the automatic generation of LOTOS
scenarios from requirements in UCM and of TGV for the automatic generation
of TTCN test suites from LOTOS. The methodology is illustrated with a
case study which is a telephony system providing the basic call feature.