A formal framework for the specification and verification of distributed processes communication flows in clouds

Job description: Clouds are constituted of servers interconnected via the Internet, on which systems can be implemented, making use of applications and databases deployed on the servers. Cloud-based computing is gaining in popularity, and that includes the context of critical systems. As a result, it is useful to define formal frameworks for reasoning about cloud-based systems. One requirement about such a framework is that it enables reasoning about the concepts manipulated in a cloud, which naturally includes the ability to reason about distributed systems, composed of subsystems deployed on different machines and interacting through message passing to implement services. In this context, the ability to reason about communication flows is central. The aim of this thesis is to define a formal framework dedicated to the specification and verification of systems deployed on clouds. This framework will capitalize on the formal framework of quot;interactionsquot;. Interactions are models dedicated to the specification of communication flows between different actors in a system. The thesis work will study how to define structuring (enrichment, composition) and refinement operators to enable the implementation of classical software engineering processes based on interactions.

Your profile: Méthodes formelles