The Accounting Model of the TINA Architecture.

Organisation:	Federal University of Santa Catarina (BRAZIL)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2001
Size:	n/a
Description:	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 Consortium. 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.
Conclusions:	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.
Publications:	[Kristiansen-97] 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
Contact:	prof. Carlos B. Westphall Federal University of Santa Catarina Technology Center Network and Management Laboratory E-mail: westphal@lrg.ufsc.br
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page