Séminaire OASIS -- 2004-2005
INRIA Sophia-Antipolis

Decembre 2004

Mercredi 15 decembre 14h00 ESSI Amphi Est

    Rabéa Boulifa INRIA Génération de modèles comportementaux des applications réparties

     Nous nous intéressons à la vérification de propriétés comportementales d'applications distribuées par la technique de model-checking. En particulier, nous étudions le problème de génération de modèles à partir de programmes Java répartis et représentés par systèmes de transitions communiquants. A partir de la sémantique formelle de programmes ProActive, une librairie 100\% Java pour la programmation parallèle, distribuée et concurrente, nous construisons, de manière compositionnelle et hiérarchique, des modèles comportementaux finis pour des abstractions finies d'applications. Ces modèles sont décrits mathématiquement et graphiquement. Et la procédure de construction, dont nous prouvons la terminaison, est décrite par des règles sémantiques s'appliquant à une forme intermédiaire des programmes obtenue par analyse statique. Ces règles sont ensuite étendues afin de générer des modèles paramétrés pour des applications possiblement infinies. La construction de modèles paramétrés a été, d'abord, faite sur un noyau de Java et la bibliothèque ProActive, puis étendue à des constructions communication de groupe. Des exemples de modèles, générés directement à partir de ces règles implémentées par un prototype, sont également étudiés.

Mercredi 15 decembre 10h30 Salle Lagrange gris

    Alessandro Fantechi Univ. De Florence Witness and Counterexample Automata for ACTL

     Witnesses and counterexamples produced by model checkers provide very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specified with a CCS-like process algebra. There, only linear and finite witnesses and counterexamples are useful and for the given formula and model an efficient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identifies a fragment of action computation tree logic (ACTL) that can be handled in this way. Moreover, a suitable form of witnesses and counterexamples is proposed and {\em witness} and {\em counterexample automata} are introduced, which are finite automata recognizing them and an algorithm for generating such automata is given. joint work with Robert Meolic (University of Maribor) and Stefania Gnesi (ISTI-CNR)

Mardi 7 decembre 14h00 Salle Euler violet E-003

    Jacques Noyé INRIA-Ecole des Mines de Nantes Composants et Aspects - si loin, si proche Slides en pdf

     Les mots qui vrombissent se succèdent à un rythme rapide et les objets ont rapidement fait place aux composants et aujourd'hui aux aspects, qui seraient la nouvelle panacée pour répondre aux besoins de la séparation des préoccupations (separation of concerns en anglais). Ces notions ont laissés sur place le terme plus ancien de module, conçu pour répondre à cette même problématique. Mais, finalement, qu'est-ce qui différencie vraiment ces différentes notions ? Nous essaierons de répondre à cette question en analysant quelques langages de composants et d'aspects significatifs.

Octobre 2004

mardi 26 octobre 11h00 Salle Lagrange gris

    Alexandre Di Costanzo Oasis / Indiana University, USA Peer-to-Peer Web Service and Firewalls

     In this presentation identify a set of common problems that exist when trying to do peer-to-peer interactions for Web Services that are behind firewalls or not generally accessible. In particular we describe methods to support reliable long running conversation through firewalls of Web Service peers that have no accessible endpoints. Our solution is to use a Web Services Dispatcher (WSD) intermediary node that forwards messages and can facilitate asynchronous communication. WSD can forward HTTP RPC connections or use WS-Addressing for asynchronous messaging between clients and Web Services. Additionally we describe how Web Services clients such as applet that can not have public endpoint can become Web Service peer by using additional message store-and-forward services provided by WSD.

vendredi 22 octobre 14h00 Salle Lagrange gris

    Eric Madelaine Oasis - INRIA "Parameterized Models for Distributed Java Objects", papier avec Tomas Barros et Rabéa Boulifa, presenté a la conference Forte'2004, Madrid, Sep. 2004, LNCS 3235.

     Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioural semantics of ProActive objects. Our models are symbolic networks of labelled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software tool set for the analysis of ProActive applications using these methods.

    Tomas Barros Oasis - INRIA "Parameterized Specification and Verification of the Chilean Electronic Invoice System", papier avec Isabelle Attali et Eric Madelaine, SCCC'04, Arica, Chili, Nov 2004

     We present the complete process of a formal specification and verification of the Chilean electronic invoice system which has been defined by the tax agency. We use this case study as a real-world and real-size example to illustrate our methodology for specification and verification of distributed applications. Our approach is based on a new hierarchical and parameterized model for synchronised networks of labelled transition systems. In this case study, we use a subset of the model as a graphical specification language. We check this formal specification of the invoice system against its informal requirements, described in terms of parameterized temporal logic formulas. Their satisfiability cannot be checked directly on the parameterized model\,: we introduce a method and a tool to instantiate the parameterized models and properties, allowing to use standard (finite-state, bisimulation-based) model-checkers for the verification. We also illustrate the use of different methods to avoid the state explosion problem by taking advantage of the parameterized structure and instantiations.

jeudi 14 octobre 14h00 Salle Fermat F102

    Léandro Léon Universidad de Los Andes, Venezuela Some Issues on the communication protocol for invocation in the Aleph system

     Most implementations of object systems base their communication mechanisms on costly protocols at the level of passing of messages. The most popular example is TCP with its excessive exchange of messages on the transport layer (or network according to OSI model). In this brief seminar, the design and implementation of a communication protocol among remote objects in the Aleph system is presented. The protocol seeks to minimize message exchange on the network and therefore to improve the performance of invocations. This protocol is based on the integration of several traditional techniques: sequence of messages, management of epochs for the treatment of failures, beatings for service delays and taking advantage of messages toward other objects for the delivery of acknowledgments. The protocol assumes an environment of large scale regarding the amount of objects and high frequency of invocations. The structure of this talk is as follows: - General description of the problem - Design of the protocol - Interface - Implementation using UDP/IP - Experiences and perspectives

Juin 2004

Mardi 17 juin 14h00 Salle du conseil

    Matthieu Morel Oasis Implantation d'un modèle de composants pour ProActive.

     Les technologies de programmation évoluent naturellement vers des niveaux d'abstraction supérieurs, ce qui facilite la conception, le développement, la configuration, et la compréhension des systèmes complexes. Les composants ont été introduits comme une nouvelle réponse à ce besoin d'abstraction. Ils peuvent être décrits comme des entités logicielles (sortes de boites noires), avec des interfaces bien définies ; ils communiquent avec leur environnement (et entre eux) au travers de ces interfaces, à l'aide d'une plate-forme de communication.
L'objectif de notre travail était d'intégrer le paradigme composant dans ProActive, afin de permettre une manipulation des objets actifs comme des composants. Pour cela, nous avons implanté dans ProActive un modèle de composants hiérarchique, extensible et dynamique, dénomme Fractal.
Je présenterai le modèle que nous avons utilisé, l'architecture de notre implantation, et les perspectives d'utilisation dans notre cadre.

    Eric Madelaine Oasis Finite Model Generation for Distributed Java Programs.

     We present techniques for analyzing the source code of distributed Java applications, and building finite models of their behaviour. The models are labelled transition systems, representing the communication events between the distributed objects. When combined with techniques for abstracting the data values used by the programs, and especially values used in the creation of distributed objects, to bounded domains, our construction terminates.
We provide models suitable for automatic verification, and typically for model checking. Moreover our models are structured in a compositionnal way, so that we can use verification techniques that scale up to applications of realistic size.

Mars 2003

Mardi 11 mars 14h00 Salle E003

    Sylvain Lippi Univ. d'Aix Marseille Théorie et pratique des réseaux d'interaction

     Les réseaux d'interaction introduits par Yves Lafont constituent un modèle de calcul asynchrone graphique issu de la théorie de la démonstration. Nous en présentons les idées essentielles en faisant une comparaison avec d'autres modèles de calcul : lambda-calcul, machines de Turing, automates cellulaires. On peut aussi considérer les réseaux comme le noyau d'un langage de programmation concurrent ne nécessitant pas de glaneur de cellules ; la gestion de la mémoire (duplication et effacement de cellules) est explicite. De plus, un interprète graphique permet de tester l'implantation avec des réseaux de différents algorithmes <> sur les listes, les tris ou l'analyse syntaxique.

Mardi 11 mars 14h00 Salle E003

    Sylvain Lippi Univ. d'Aix Marseille Théorie et pratique des réseaux d'interaction

     Les réseaux d'interaction introduits par Yves Lafont constituent un modèle de calcul asynchrone graphique issu de la théorie de la démonstration. Nous en présentons les idées essentielles en faisant une comparaison avec d'autres modèles de calcul : lambda-calcul, machines de Turing, automates cellulaires. On peut aussi considérer les réseaux comme le noyau d'un langage de programmation concurrent ne nécessitant pas de glaneur de cellules ; la gestion de la mémoire (duplication et effacement de cellules) est explicite. De plus, un interprète graphique permet de tester l'implantation avec des réseaux de différents algorithmes <> sur les listes, les tris ou l'analyse syntaxique.

Mardi 4 Mars 10h40 Salle du conseil

    Guillermo Lama Oasis Distributed Garbage collection in an ActiveObject Environment

     Resource managment in computer is a tedious task, and in a networked environment it's an exhaustive work for programmers too. Distributed Garbage Collection try to absolve the developer from tracking memory and resource usage in a Active Object environment. Mainly it is supposed to detect unused resources, and in our case, must support object migration. Many of the usual algorithms that perform Garbage Collection are for passive objects. Our goal is to implement a DGC (Distributed Garbage Collector) using IRC (Indirect Reference Count Algorithm) and if necessary perform some modifications to ensure garbage collection for Active Objects. Some attractive point is that IRC algorithm supposes good behavior in losely-coupled distributed environments. Uses of soft-state techniques will be considered for possible for performance improvements. The DGC prototype is supposed to be implmented for the ProActive library, independently of the transport layer, considering the present operation of the RMI-DGC and a possible interaction with our DGC. Regarding that the DGC must be comprehensive, correct, expedient and efficient. The work must achieve a tunnable DGC that probably will combine several garbage collection techniques mainly adapted for structures like Network Objects.

Eric Madelaine

Last modified: Tue Dec 10 18:11:58 MET 2002

Talks in 2002
Talks in 2001
Talks in 2000
Talks in 1999
Retour au serveur du projet / Back to the OASIS main page

Decembre 2004
Mercredi 15 decembre	14h00	ESSI Amphi Est
Rabéa Boulifa	INRIA	Génération de modèles comportementaux des applications réparties
		Nous nous intéressons à la vérification de propriétés comportementales d'applications distribuées par la technique de model-checking. En particulier, nous étudions le problème de génération de modèles à partir de programmes Java répartis et représentés par systèmes de transitions communiquants. A partir de la sémantique formelle de programmes ProActive, une librairie 100\% Java pour la programmation parallèle, distribuée et concurrente, nous construisons, de manière compositionnelle et hiérarchique, des modèles comportementaux finis pour des abstractions finies d'applications. Ces modèles sont décrits mathématiquement et graphiquement. Et la procédure de construction, dont nous prouvons la terminaison, est décrite par des règles sémantiques s'appliquant à une forme intermédiaire des programmes obtenue par analyse statique. Ces règles sont ensuite étendues afin de générer des modèles paramétrés pour des applications possiblement infinies. La construction de modèles paramétrés a été, d'abord, faite sur un noyau de Java et la bibliothèque ProActive, puis étendue à des constructions communication de groupe. Des exemples de modèles, générés directement à partir de ces règles implémentées par un prototype, sont également étudiés.
Mercredi 15 decembre	10h30	Salle Lagrange gris
Alessandro Fantechi	Univ. De Florence	Witness and Counterexample Automata for ACTL
		Witnesses and counterexamples produced by model checkers provide very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specified with a CCS-like process algebra. There, only linear and finite witnesses and counterexamples are useful and for the given formula and model an efficient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identifies a fragment of action computation tree logic (ACTL) that can be handled in this way. Moreover, a suitable form of witnesses and counterexamples is proposed and {\em witness} and {\em counterexample automata} are introduced, which are finite automata recognizing them and an algorithm for generating such automata is given. joint work with Robert Meolic (University of Maribor) and Stefania Gnesi (ISTI-CNR)
Mardi 7 decembre	14h00	Salle Euler violet E-003
Jacques Noyé	INRIA-Ecole des Mines de Nantes	Composants et Aspects - si loin, si proche Slides en pdf
		Les mots qui vrombissent se succèdent à un rythme rapide et les objets ont rapidement fait place aux composants et aujourd'hui aux aspects, qui seraient la nouvelle panacée pour répondre aux besoins de la séparation des préoccupations (separation of concerns en anglais). Ces notions ont laissés sur place le terme plus ancien de module, conçu pour répondre à cette même problématique. Mais, finalement, qu'est-ce qui différencie vraiment ces différentes notions ? Nous essaierons de répondre à cette question en analysant quelques langages de composants et d'aspects significatifs.
Octobre 2004
mardi 26 octobre	11h00	Salle Lagrange gris
Alexandre Di Costanzo	Oasis / Indiana University, USA	Peer-to-Peer Web Service and Firewalls
		In this presentation identify a set of common problems that exist when trying to do peer-to-peer interactions for Web Services that are behind firewalls or not generally accessible. In particular we describe methods to support reliable long running conversation through firewalls of Web Service peers that have no accessible endpoints. Our solution is to use a Web Services Dispatcher (WSD) intermediary node that forwards messages and can facilitate asynchronous communication. WSD can forward HTTP RPC connections or use WS-Addressing for asynchronous messaging between clients and Web Services. Additionally we describe how Web Services clients such as applet that can not have public endpoint can become Web Service peer by using additional message store-and-forward services provided by WSD.
vendredi 22 octobre	14h00	Salle Lagrange gris
Eric Madelaine	Oasis - INRIA	"Parameterized Models for Distributed Java Objects", papier avec Tomas Barros et Rabéa Boulifa, presenté a la conference Forte'2004, Madrid, Sep. 2004, LNCS 3235.
		Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioural semantics of ProActive objects. Our models are symbolic networks of labelled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software tool set for the analysis of ProActive applications using these methods.
Tomas Barros	Oasis - INRIA	"Parameterized Specification and Verification of the Chilean Electronic Invoice System", papier avec Isabelle Attali et Eric Madelaine, SCCC'04, Arica, Chili, Nov 2004
		We present the complete process of a formal specification and verification of the Chilean electronic invoice system which has been defined by the tax agency. We use this case study as a real-world and real-size example to illustrate our methodology for specification and verification of distributed applications. Our approach is based on a new hierarchical and parameterized model for synchronised networks of labelled transition systems. In this case study, we use a subset of the model as a graphical specification language. We check this formal specification of the invoice system against its informal requirements, described in terms of parameterized temporal logic formulas. Their satisfiability cannot be checked directly on the parameterized model\,: we introduce a method and a tool to instantiate the parameterized models and properties, allowing to use standard (finite-state, bisimulation-based) model-checkers for the verification. We also illustrate the use of different methods to avoid the state explosion problem by taking advantage of the parameterized structure and instantiations.
jeudi 14 octobre	14h00	Salle Fermat F102
Léandro Léon	Universidad de Los Andes, Venezuela	Some Issues on the communication protocol for invocation in the Aleph system
		Most implementations of object systems base their communication mechanisms on costly protocols at the level of passing of messages. The most popular example is TCP with its excessive exchange of messages on the transport layer (or network according to OSI model). In this brief seminar, the design and implementation of a communication protocol among remote objects in the Aleph system is presented. The protocol seeks to minimize message exchange on the network and therefore to improve the performance of invocations. This protocol is based on the integration of several traditional techniques: sequence of messages, management of epochs for the treatment of failures, beatings for service delays and taking advantage of messages toward other objects for the delivery of acknowledgments. The protocol assumes an environment of large scale regarding the amount of objects and high frequency of invocations. The structure of this talk is as follows: - General description of the problem - Design of the protocol - Interface - Implementation using UDP/IP - Experiences and perspectives
Juin 2004
Mardi 17 juin	14h00	Salle du conseil
Matthieu Morel	Oasis	Implantation d'un modèle de composants pour ProActive.
		Les technologies de programmation évoluent naturellement vers des niveaux d'abstraction supérieurs, ce qui facilite la conception, le développement, la configuration, et la compréhension des systèmes complexes. Les composants ont été introduits comme une nouvelle réponse à ce besoin d'abstraction. Ils peuvent être décrits comme des entités logicielles (sortes de boites noires), avec des interfaces bien définies ; ils communiquent avec leur environnement (et entre eux) au travers de ces interfaces, à l'aide d'une plate-forme de communication. L'objectif de notre travail était d'intégrer le paradigme composant dans ProActive, afin de permettre une manipulation des objets actifs comme des composants. Pour cela, nous avons implanté dans ProActive un modèle de composants hiérarchique, extensible et dynamique, dénomme Fractal. Je présenterai le modèle que nous avons utilisé, l'architecture de notre implantation, et les perspectives d'utilisation dans notre cadre.
Eric Madelaine	Oasis	Finite Model Generation for Distributed Java Programs.
		We present techniques for analyzing the source code of distributed Java applications, and building finite models of their behaviour. The models are labelled transition systems, representing the communication events between the distributed objects. When combined with techniques for abstracting the data values used by the programs, and especially values used in the creation of distributed objects, to bounded domains, our construction terminates. We provide models suitable for automatic verification, and typically for model checking. Moreover our models are structured in a compositionnal way, so that we can use verification techniques that scale up to applications of realistic size.
Mars 2003
Mardi 11 mars	14h00	Salle E003
Sylvain Lippi	Univ. d'Aix Marseille	Théorie et pratique des réseaux d'interaction
		Les réseaux d'interaction introduits par Yves Lafont constituent un modèle de calcul asynchrone graphique issu de la théorie de la démonstration. Nous en présentons les idées essentielles en faisant une comparaison avec d'autres modèles de calcul : lambda-calcul, machines de Turing, automates cellulaires. On peut aussi considérer les réseaux comme le noyau d'un langage de programmation concurrent ne nécessitant pas de glaneur de cellules ; la gestion de la mémoire (duplication et effacement de cellules) est explicite. De plus, un interprète graphique permet de tester l'implantation avec des réseaux de différents algorithmes <> sur les listes, les tris ou l'analyse syntaxique.
Mardi 11 mars	14h00	Salle E003
Sylvain Lippi	Univ. d'Aix Marseille	Théorie et pratique des réseaux d'interaction
		Les réseaux d'interaction introduits par Yves Lafont constituent un modèle de calcul asynchrone graphique issu de la théorie de la démonstration. Nous en présentons les idées essentielles en faisant une comparaison avec d'autres modèles de calcul : lambda-calcul, machines de Turing, automates cellulaires. On peut aussi considérer les réseaux comme le noyau d'un langage de programmation concurrent ne nécessitant pas de glaneur de cellules ; la gestion de la mémoire (duplication et effacement de cellules) est explicite. De plus, un interprète graphique permet de tester l'implantation avec des réseaux de différents algorithmes <> sur les listes, les tris ou l'analyse syntaxique.
Mardi 4 Mars	10h40	Salle du conseil
Guillermo Lama	Oasis	Distributed Garbage collection in an ActiveObject Environment
		Resource managment in computer is a tedious task, and in a networked environment it's an exhaustive work for programmers too. Distributed Garbage Collection try to absolve the developer from tracking memory and resource usage in a Active Object environment. Mainly it is supposed to detect unused resources, and in our case, must support object migration. Many of the usual algorithms that perform Garbage Collection are for passive objects. Our goal is to implement a DGC (Distributed Garbage Collector) using IRC (Indirect Reference Count Algorithm) and if necessary perform some modifications to ensure garbage collection for Active Objects. Some attractive point is that IRC algorithm supposes good behavior in losely-coupled distributed environments. Uses of soft-state techniques will be considered for possible for performance improvements. The DGC prototype is supposed to be implmented for the ProActive library, independently of the transport layer, considering the present operation of the RMI-DGC and a possible interaction with our DGC. Regarding that the DGC must be comprehensive, correct, expedient and efficient. The work must achieve a tunnable DGC that probably will combine several garbage collection techniques mainly adapted for structures like Network Objects.

Séminaire OASIS -- 2004-2005 INRIA Sophia-Antipolis

Séminaire OASIS -- 2004-2005
INRIA Sophia-Antipolis