Génération de modèles comportemementaux des applications des applications réparties
Rabéa Ameur-Boulifa · HAL (Le Centre pour la Communication Scientifique Directe) · 2004
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.