Formal verification methods are increasingly being used in industry to establish the correctness of, and to find the flaws in, system models. We use equivalence reasoning and formal sequentialization via internal communication elimination. It is based on the application of a set of laws, as rewriting reductions to a system model.

This theory is based following the same semantics as Manna and Pnueli for reactive systems. We carry out equivalence proofs based on formal communication elimination  for the simplification of distributed system models via application of accepted equivalence laws.

For more information about this topic, please contact Dr. Miquel Bertran.

In the area of distributed systems, we work on the design, model and simulation of concurrency control algorithms applied to database with transaction management. We focus on the study  of algorithms with different levels of replication, fragmentation and placement, support of unicast and total order networks.

We do also design distributed information systems with optimal access to information, applied to transactional and analytical systems. This includes the evaluation of platforms for Write One Read Many (WORM) systems, monitoring cloud systems and services to business intelligence systems.

For more information about this topic, please contact Dr. August Climent.