Federal University of Santa Catarina (BRAZIL)
CADP (Construction and Analysis of Distributed Processes)
TINA (Telecommunications Information Networking Architecture)
was created by the TINA-C consortium, made up of over 40 companies,
among which telecommunication operators and software vendors. TINA
aims at defining a global architecture for advanced telecommunication
systems. TINA consists basically of a business model and a service
architecture. The business model defines a framework for specifying
reference points and roles, and for propagating requirements in a TINA
system. The service architecture is a set of concepts and principles
for developing TINA services and operate with them. The TINA
architecture is currently under standardization within the TINA-C
According to the specifications given by the TINA-C Consortium, the accounting management of TINA consists basically of four phases: metering (recording the use of resources), classification (grouping the metering information into a set of classes based on usage of service, types of resources, etc.), tariffing (calculation of the charge based upon the classification and the tariff structure), and billing (storing the charge information and sending it to a consumer).
The LOTOS specification of the TINA service architecture corresponds to a formalization of the interaction between a user and a TINA model through a reference point. This interaction consists of an access part and a use part; the access part has been completely specified in LOTOS, whereas in the use part only the accounting management was specified. The Labeled Transition Systems corresponding to the interaction protocol and to its external behaviour (service) have been generated with the CAESAR compiler and verified to be observationally equivalent with the ALDEBARAN tool of CADP.
An important part of the service architecture of TINA (including the
accounting management) was specified in LOTOS and verified using the
CADP toolbox. This effort produced a formal reference model of TINA,
which can profitably be used for the analysis and development of other
management functions of TINA.
L. Kristiansen. "TINA Service Architecture 5.0".
TINA-C Consortium, 1997.
[Rossi-Souza-Sekkaki-Westphall-01] L. L. Rossi, I. V. de Souza, A. Sekkaki, and C. B. Westphall. "Formal Specification and Verification of the Accounting Model of TINA Architecture using LOTOS and ALDEBARAN". Proceedings of the Congresso Brasileiro de Computacao, Itajai (Santa Catarina, Brazil), August 2001.
Available on-line from the CADP Web site in PDF or PostScript
prof. Carlos B. Westphall
Federal University of Santa Catarina
Network and Management Laboratory
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies