Formalization of Service Creation in Intelligent Network

M.-P. Gervais, A. Diagne

LIP6 1997/012: Rapport de Recherche LIP6 / LIP6 research reports
6 pages - Juillet/July 1997 - Document en anglais.

PostScript : 732 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Formalisation de la création de services dans le réseau intelligent
Titre anglais : Formalization of Service Creation in Intelligent Network

Résumé : La création de service dans le réseau intelligent est un problème de qualité du logiciel qui inclut les activités d'analyse, conception, implantation, déploiement et maintenance. Afin d'assurer cette qualité, la validation et la vérification formelle de la spécification sont nécessaires. La validation d'un service consiste à vérifier la cohérence globale de son analyse et de sa conception tandis que la vérification consiste en la preuve formelle de propriétés structurelles et comportementales que l'on en attend.
Nous proposons dans ce papier une approche multi-formalismes, couplant l'utilisation des paradigmes orienté-objet et réseau de Petri, qui permet à un concepteur de valider et vérifier une spécification de service. Nous mettons à sa disposition un outil de preuve lui permettant de réaliser ces activités. Ce papier décrit cet outil de preuve et ainsi qu'un exemple de son utilisation.

Abstract : The service creation in Intelligent Network is a software quality problem that encompasses several activities, namely specification, design, implementation, deployment and maintenance. In order to ensure the software quality, validation and formal verification are required. Validation of a service consists of verifying the global coherence of its specification and design, while verification consists of formal proof of structural and behavioral expected properties.
We propose in this paper a multi-formalism approach, coupling the use of Object-Oriented (OO) and Petri Nets (PN) paradigms, which enables a designer to validate and to verify a service specification. We provide him a proving toolset in order to achieve these activities. This paper describes this proving toolset and its experience on an exemple.

Mots-clés : réseau intelligent, service de télécommunication, création de service, paradigme orienté-objet, réseau de Petri, validation, vérification, outil de preuve

Key-words : Intelligent Network, Telecommunication Service, Service Creation, Object-Oriented Paradigm, Petri Nets, Validation, Verification, Proving Toolset

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr