Model Generation for distributed programs.
Génération de modèles comportemementaux des applications des applications réparties
Résumé
Therefore, we define a behavioural semantics for ProActive, a Java library for concurrent, distributed,
and mobile computing. From this semantics we
build behavioural models for finite abstractions of applications. These models are based on
process algebra semantics, so they can be built in a compositional
manner.
Building the finite models is not always possible.
In order to deal the problems that take into account the data as well the
problems concerning topologies with infinite objects, we define the
notion of hierarchical models, based on parameterized transition
systems and parameterized synchronisation networks.
By means of abstractions these models can depict infinite
applications by expressive and finite representations.
On the other hand, we define a system of semantics rules for
building the (finite or parameterized) models from an
intermediate form of programs obtained by static analysis.
The models generated this way are used directly or after instantiation, standard
by verification tools.
and mobile computing. From this semantics we
build behavioural models for finite abstractions of applications. These models are based on
process algebra semantics, so they can be built in a compositional
manner.
Building the finite models is not always possible.
In order to deal the problems that take into account the data as well the
problems concerning topologies with infinite objects, we define the
notion of hierarchical models, based on parameterized transition
systems and parameterized synchronisation networks.
By means of abstractions these models can depict infinite
applications by expressive and finite representations.
On the other hand, we define a system of semantics rules for
building the (finite or parameterized) models from an
intermediate form of programs obtained by static analysis.
The models generated this way are used directly or after instantiation, standard
by verification tools.
Dans notre travail nous nous sommes intéressés à la vérification
automatique de propriétés comportementales d'applications réparties par des
méthodes fondées sur les
modèles. 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 des systèmes de transitions
communiquants.
Pour ce faire, nous définissons une sémantique comportementale de programmes ProActive, une
librairie Java pour la programmation parallèle, distribuée et
concurrente. À partir de cette sémantique nous construisons des modèles
comportementaux pour
des abstractions finies d'applications écrites dans ce langage. Ces
modèles sont basés sur la sémantique des algèbres de
processus et peuvent donc être construits de manière compositionnelle et
hiérarchique.
La construction de modèles finis n'est pas toujours possible. Pour
pouvoir traiter des problèmes prenant en compte des données, ainsi que
des problèmes concernant des topologies non bornées d'objets
répartis, nous définissons une nouvelle notion de modèleles
hiérarchiques, à base de systèmes de transitions paramétrés et de
réseau de synchronisation paramétrés. Moyennant des abstractions ces modèles permettent de
spécifier des applications possiblement infinies par des représentations
expressives, finies, et plus proche de la structure du code.
Par ailleurs, nous définissons un système de règles sémantiques
permettant de générer automatiquement ces modèles (finis ou
paramétrés) à partir d'une forme intermédiaire, obtenue par analyse statique,
des programmes analysés.
Les modèles ainsi générés sont exploitables directement ou après
instantiation par des outils de vérification.
automatique de propriétés comportementales d'applications réparties par des
méthodes fondées sur les
modèles. 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 des systèmes de transitions
communiquants.
Pour ce faire, nous définissons une sémantique comportementale de programmes ProActive, une
librairie Java pour la programmation parallèle, distribuée et
concurrente. À partir de cette sémantique nous construisons des modèles
comportementaux pour
des abstractions finies d'applications écrites dans ce langage. Ces
modèles sont basés sur la sémantique des algèbres de
processus et peuvent donc être construits de manière compositionnelle et
hiérarchique.
La construction de modèles finis n'est pas toujours possible. Pour
pouvoir traiter des problèmes prenant en compte des données, ainsi que
des problèmes concernant des topologies non bornées d'objets
répartis, nous définissons une nouvelle notion de modèleles
hiérarchiques, à base de systèmes de transitions paramétrés et de
réseau de synchronisation paramétrés. Moyennant des abstractions ces modèles permettent de
spécifier des applications possiblement infinies par des représentations
expressives, finies, et plus proche de la structure du code.
Par ailleurs, nous définissons un système de règles sémantiques
permettant de générer automatiquement ces modèles (finis ou
paramétrés) à partir d'une forme intermédiaire, obtenue par analyse statique,
des programmes analysés.
Les modèles ainsi générés sont exploitables directement ou après
instantiation par des outils de vérification.