2 resultados para compositional models

em AMS Tesi di Dottorato - Alm@DL - Università di Bologna


Relevância:

60.00% 60.00%

Publicador:

Resumo:

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.

Relevância:

30.00% 30.00%

Publicador:

Resumo:

The aim of this Thesis is to investigate the effect of heterogeneities within the subducting plate on the dynamics of subduction. In particular, I study the motion of the trench for oceanic and continental subduction, first, separately, and, then, together in the same system to understand how they interact. The understanding of these features is fundamental to reconstruct the evolution of complex subduction zones, such as the Central Mediterranean. For this purpose, I developed 2D and 3D numerical models of oceanic and continental subduction where the rheological, geometrical and compositional properties of the plates are varied. In these models, the trench and the overriding plate move self-consistently as a function of the dynamics of the system. The effect of continental subduction on trench migration is largely investigated. Results from a parametric study showed that despite different rheological properties of the plates, all models with a uniform continental crust share the same kinematic behaviour: the trench starts to advance once the continent arrives at the subduction zone. Hence, the advancing mode in continental collision scenarios is at least partly driven by an intrinsic feature of the system. Moreover, the presence of a weak lower crust within the continental plate can lead to the occurrence of delamination. Indeed, by changing the viscosity of the lower crust, both delamination and slab detachment can occur. Delamination is favoured by a low viscosity value of the lower crust, because this makes the mechanical decoupling easier between crust and lithospheric mantle. These features are observed both in 2D and 3D models, but the numerical results of the 3D models also showed that the rheology of the continental crust has a very strong effect on the dynamics of the whole system, since it influences not only the continental part of plate but also the oceanic sides.