Formal specification and verification of distributed data structures
The future of the computing technology relies on fast access, transformation, and exchange of data across large-scale networks such as the Internet. The design of software systems that support high-frequency parallel accesses to h...
ver más
¿Tienes un proyecto y buscas un partner? Gracias a nuestro motor inteligente podemos recomendarte los mejores socios y ponerte en contacto con ellos. Te lo explicamos en este video
Proyectos interesantes
RELAX
Relaxed Semantics Across the Data Analytics Stack
Cerrado
TIN2013-46928-C3-1-R
PRUEBAS DE LA PERSISTENCIA DE DATOS Y PERSPECTIVA DE USUARIO...
149K€
Cerrado
UncertainENV
The Power of Randomization in Uncertain Environments
2M€
Cerrado
FADAMS
Foundations of Factorized Data Management Systems
2M€
Cerrado
TIN2012-37954
ALGORITMOS DE APRENDIZAJE COMPUTACIONAL EN ENTORNOS DISTRIBU...
135K€
Cerrado
TIN2017-88614-R
ESPACIO DE DIRECCIONES PARTICIONADO, COMUNICADO Y ESCALABLE...
84K€
Cerrado
Información proyecto FOVEDIS
Duración del proyecto: 70 meses
Fecha Inicio: 2015-12-18
Fecha Fin: 2021-10-31
Líder del proyecto
UNIVERSITE PARIS CITE
No se ha especificado una descripción o un objeto social para esta compañía.
TRL
4-5
Presupuesto del proyecto
1M€
Fecha límite de participación
Sin fecha límite de participación.
Descripción del proyecto
The future of the computing technology relies on fast access, transformation, and exchange of data across large-scale networks such as the Internet. The design of software systems that support high-frequency parallel accesses to high-quantity data is a fundamental challenge. As more scalable alternatives to traditional relational databases, distributed data structures (DDSs) are at the basis of a wide range of automated services, for now, and for the foreseeable future.
This proposal aims to improve our understanding of the theoretical foundations of DDSs. The design and the usage of DDSs are based on new principles, for which we currently lack rigorous engineering methodologies. Specifically, we lack design procedures based on precise specifications, and automated reasoning techniques for enhancing the reliability of the engineering process.
The targeted breakthrough of this proposal is developing automated formal methods for rigorous engineering of DDSs. A first objective is to define coherent formal specifications that provide precise requirements at design time and explicit guarantees during their usage. Then, we will investigate practical programming principles, compatible with these specifications, for building applications that use DDSs. Finally, we will develop efficient automated reasoning techniques for debugging or validating DDS implementations against their specifications. The principles underlying automated reasoning are also important for identifying best practices in the design of these complex systems to increase confidence in their correctness. The developed methodologies based on formal specifications will thus benefit both the conception and automated validation of DDS implementations and the applications that use them.