Nos partenaires



Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe ACADIE > Recherches

Verification of Critical Distributed Systems

The group’s themes are : specification and verification of data-directed distributed real-time systems and Distributed services discovery and composition. The strong points of both subjects are : Synchronous/asynchronous distributed models, combined semantic and behavioral system description, real-time constraints used as QoS properties and temporal and architectural properties verification.

Specification and verification of data-directed distributed real-time systems.

These works were initiated during the 2007-2009 years and has been continued in the last period during which two theses have been defended on this subject. Our application domain is DRE (Distributed Real-time Embedded) systems, which merge distributed algorithms, real time systems and embedded systems. Our approach is to consider a data-directed description of systems, without considering the traditional decomposition in tasks and its scheduling problems. This approach considers how data flow and what real time and logical consistency properties are expected. Using an abstract specification of interactions, we have shown how to automatically verify the feasibility w.r.t. to temporal constraints (freshness, latency...). We have formalized and solved the problem of input inconsistency when multiple information paths exist in a multi-periodic component system. We have also studied the definition and the control of the time predictability of communication through a software transactional memory. A common question has arisen with regard to synchronous and asynchronous models : real time system and predictability results are often given in a synchronous model, whereas complex distributed systems are often asynchronous. Concretely, we have considered the GALS (globally asynchronous, locally synchronous) approach which maps to many-core architectures as well as distributed multi-core architectures, and abstractly, we are studying the unification of various synchronous and asynchronous communication models.

Distributed services discovery and composition

Work has continued on services discovery and composition. Initially, we have considered signature and functional specifications, using an algebraic description. This work has been completed by the selection of the most appropriate compositions based on QoS criteria, has been integrated in a middleware, and is currently being certified with Coq. The acquired expertise has been applied to a platform on scientific computation. Besides, we are also taking into account the behavioral descriptions and are considering QoS, especially real time properties. Collaborations with other teams have yield results regarding behavioral compatibility in the synchronous model and in one specific asynchronous communication model ; our current work investigates other asynchronous models.