precise.project

PRECISE Research Project

Project Name: PRECISE - A correct by design methodology for available cloud applications
Funding Institution: Fundação para a Ciência e Tecnologia
Project Reference: PTDC/CCI-INF/32081/2017
Principal Investigator: Carla Ferreira
Leading Institution: NOVA.ID.FCT - Associação para a Inovação e Desenvolvimento da Faculdade de Ciências e Tecnologia
Other Institutions: NOVA SST - NOVA School of Science and Technology
NOVA LINCS - NOVA Laboratory for Informatics and Computer Science
Project Duration: 01-10-2018 to 30-09-2021
Total Funding: 228.237,65 €

Project Abstract

Cloud applications are increasingly fragmented into aggregations of micro-services that organically cooperate with each other. Ensuring consistency between cooperating services raises new challenges: related data is scattered across services; services might have heterogenous consistency models; cross-service operations cannot rely on the atomicity and isolation properties available when using a single data store. Our vision is to propose language-based analysis techniques to validate the application service orchestration and to derive the minimum synchronisation among these services. With our approach, developers no longer have to rely on complex and ad-hoc reasoning to validate an application. We aim to provide efficient analysis techniques to detect anomalous cross-service interactions. Integrating these techniques in the development life-cycle will increase the developer’s productivity and improve service quality in terms of efficiency, availability and correctness.

Research Team

Carla Ferreira (Principal Investigator)
Nuno Preguiça (Co-Principal Investigator)
João Costa Seco (Reseacher)
Miguel Goulão (Reseacher)Sérgio Duarte (Reseacher)
Mário Pereira (Researcher)
Catarina Gralha (Post-doc)
Ana Catarina Ribeiro (PhD student)
Filipe Meirim (PhD student)
Hugo Rodrigues (MSc student)
Dina Borrego (MSc student)
Rodrigo Ribeiro (MSc student)
João Figueira (MSc student)
Sara Simões (MSc student)
Gualter Parada (MSc student)
Nuno Gomes (MSc student)

Publications

Journals

• Hugo Lourenço, Carla Ferreira, João Costa Seco, et al. OSTRICH: a rich template language for low-code development (extended version). Softw Syst Model (2022). [Publisher Website]
• João Costa Seco, Paulo Ferreira, Hugo Lourenço, Carla Ferreira, Lúcio Ferrão: Robust Contract Evolution in a TypeSafe MicroServices Architecture. Art Sci. Eng. Program. 4(3): 10 (2020). [Publisher Website]

International Conferences

• Kevin De Porre, Carla Ferreira, Elisa Gonzalez Boix: VeriFx: Correct Replicated Data Types for the Masses. ECOOP 2023 (to appear). [Publisher Website]
• João Costa Seco, Hugo Lourenço, Joana Parreira, Carla Ferreira: Nested OSTRICH: hatching compositions of low-code templates. MoDELS 2022: 210-220. [Publisher Website]
• Hugo Lourenço, Carla Ferreira and João Costa Seco, “OSTRICH - A Type-Safe Template Language for Low-Code Development,” 2021 ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS), Fukuoka, Japan, 2021, pp. 216-226. [Publisher Website]
• B. Lopes, S. Amorim and C. Ferreira, “Solution Discovery over Feature Toggling with Built-in Abstraction in OutSystems,” 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), Fukuoka, Japan, 2021, pp. 47-56. [Publisher Website]
• Alexandre Jacinto, Miguel Lourenço, and Carla Ferreira. 2020. Test mocks for low-code applications built with OutSystems. In Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings (MODELS ‘20). Association for Computing Machinery, New York, NY, USA, Article 75, 1–5. [Publisher Website]
• Peter Zeller, Annette Bieniusa, and Carla Ferreira. 2020. Teaching practical realistic verification of distributed algorithms in Erlang with TLA+. In Proceedings of the 19th ACM SIGPLAN International Workshop on Erlang (Erlang 2020). Association for Computing Machinery, New York, NY, USA, 14–23. [Publisher Website]
• Carla Ferreira. 2019. Techniques for safe and highly available cloud applications. In Proceedings of the 6th Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC ‘19). Association for Computing Machinery, New York, NY, USA, Article 1, 1–2. [Publisher Website]
• Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno Preguiça. 2018. IPA: invariant-preserving applications for weakly consistent replicated databases. Proc. VLDB Endow. 12, 4 (December 2018), 404–418. [Publisher Website]

International publications under revision

• João Costa Seco, Hugo Lourenço, Joana Parreira, Carla Ferreira: Nested OSTRICH: hatching compositions of low-code templates (extended version). Submitted to journal of Softw Syst Model.
• Dina Borrego, Carla Ferreira, and Nuno Preguiça: How to Enforce and Verify Invariants in Weakly Consistent Databases. Submitted to PaPoC 2023.
• Saalik Hatia, Annette Bieniusa, Carla Ferreira, and Marc Shapiro: From specification to implementation of a database backend. Submitted to Systor 2023.

National Conferences

• Dina Borrego, Carla Ferreira, and Nuno Preguiça. “Verificação e Reforço de Invariantes Aplicacionais no Antidote SQL”. In: INForum Simpósio de Informática (INForum 2022). 2022.
• Constança Manteigas, Joana Parreira, João Costa Seco, and Carla Ferreira. “Type-Safe Customization of Low-code Templates”. In: INForum Simpósio de Informática (INForum 2022). 2022.
• Sara Simões, Ana Ribeiro, Carla Ferreira, and Nuno Preguiça. “JepREST: Teste Funcional de Aplicações REST Distribuídas”. In: INForum Simpósio de Informática (INForum 2021). 2021.
• Filipe Meirim, Mário Pereira, and Carla Ferreira. “CISE3: Verificação de aplicações com consistência fraca em Why3”. In: INForum Simpósio de Informática (INForum 2019). 2019.

Technical Reports

• Sreeja Nair, Filipe Meirim, Mário Pereira, Carla Ferreira, and Marc Shapiro: A coordination-free, convergent, and safe replicated tree. [ArXiv Page]
• Filipe Meirim, Mário Pereira, and Carla Ferreira: CISE3: Verifying Weakly Consistent Applications with Why3. [ArXiv Page]
• Pedro Lopes, João Sousa, Valter Balegas, Carla Ferreira, Ségio Duarte, Annette Bieniusa, Rodrigo Rodrigues, and Nuno Preguiça: Antidote SQL: Relaxed When Possible, Strict When Necessary. [ArXiv Page]

Thesis

Hugo Rodrigues (2021 - 2022).
Thesis: Causal consitency verification in RESTful systems. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Dina Borrego (2021 — 2022).
Thesis: Verifying and Enforcing Application Constraints in Antidote SQL. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Rodrigo Ribeiro (2021 — 2022).
Thesis: Contract Evolution in a MicroServices Architecture. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

João Figueira (2020 — 2021).
Thesis: A Verification Technique for CRDTs in Rust. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Sara Simões (2020 — 2021).
Thesis: JepREST: Functional Testing of Distributed RESTful Applications. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Tomás Silva (2020 — 2021).
Thesis: Monitoring Road Traffic Rules with Spatio-Temporal Properties. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Ana Catarina Ribeiro (2019 — 2020).
Thesis: Invariant-Driven Automated Testing. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Gualter Parada (2019 — 2020).
Thesis: Inferring Likely Data Invariants. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Nuno Gomes (2019 — 2020).
Thesis: A Semantic Consistency Model to Reduce Coordination in Replicated Systems. Mestrado em Engenharia Informática, Universidade NOVA Lisboa.

Prototypes and Software

• VeryFx Specialized programming language for building RDTs with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala and JavaScript). VeriFx provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties.
• ECROS Framework supporting replicated datatypes to be derived from sequential data types, based on a distributed specification that declares the application semantics by means of invariants over the replicated state. Includes Ordana analysis tool, supporting middleware, and datatypes portfolio.
• PETIT Black-box testing tool that fully automates the microservice testing process when the source code is unavailable, and the only information accessible is the OAS document, written in JSON and properly extended with APOSTL contracts, automatically generated by the APOSTLGen tool. These contracts define the state invariants, pre- and post-conditions written at the cost of GET operations.
• CEC Tool, based on the CISE theory, designed to help programmers develop weakly consistent application.

Events

The project team was involved in the organization of the following events:

• Dagstuhl Seminar on Programming Languages for Distributed Systems and Distributed Data Management The goal of this seminar was to discuss the language abstractions that enable developers to tackle challenges as consistency, concurrency, and fault tolerance, among others. Organised by Carla Ferreira, Philipp Haller, Volker Markl, Guido Salvaneschi, and Cristina Videira Lopes. Dagstuhl Seminar 19442. October 2019.
• Encontro Nacional de Sistemas Distribuídos First Portuguese meeting for the research community in distributed systems. Organized by Luis Rodrigues and Nuno Preguiça et al. June 2022.

This site is open source. Improve this page.