T-LADIES

Project PRIN 2020TL3X8X.

Funded by Ministero dell'Università e della Ricerca from June 1st, 2022 to May 31st, 2025 (36 months).

Principal Investigator: Walter Cazzola

Brief description of the project

The novel Horizon Europe Programme targets the development of advanced technologies, formal methods and tools for reliable and efficient distributed applications in cloud-to-edge-to-IoT systems. Conventional language and engineering techniques struggle to keep up with the pace at which such applications evolve and provide inadequate support for development/maintenance, automatic property verification/enforcement and bug detection.

T-LADIES has 3 pillars:

  1. LANGUAGE ADAPTATION as a flexible and noninvasive mechanism for the adaptation of complex applications to different scenarios
  2. INTERACTION MECHANISMS as cornerstones for modular development of complex and evolving applications
  3. ADVANCED TYPE SYSTEMS for the specification of entities, error detection and type-driven application synthesis

LANGUAGE ADAPTATION

The idea is to lift traditional SW requirements for code flexibility, adaptability and modularity to the programming language itself to free developers from forecasting context-dependent properties at development time. Language workbenches like Xtext, Neverlang and micro-languages will be used to develop domain-specific languages (DSL) for SW dynamic evolution and property tuning via the adaptation of the language itself.

INTERACTION MECHANISMS

Modern SW applications consist of loosely connected, distributed, possibly heterogeneous interacting entities, like IoT applications of a varying number of context-sensitive devices interconnected by a network with a dynamic topology. This requires high-level interaction mechanisms and entity orchestration to address correctness, evolution and dynamic adaptation. The agent metaphor allows to achieve the right level of abstraction for interactions between low-level entities and high-level applications.

ADVANCED TYPE SYSTEMS

Types are used to specify the expected behavior of interacting entities to detect errors that may compromise correctness. They need to be easily adaptable to different scenarios and support the process of SW development and evolution to 1) enable forms of integration between static type checking and runtime verification; 2) devise automated ways to assemble complex applications and synthesize rule engines.

Structure

T-LADIES has 3 work packages mirroring the pillars and a 4th one provides challenging scenarios to drive the research and experiment with the outcome. The project is based on recent advances, some provided by the participants, who bring complementary skills and a history of joint work. The funding will strengthen existing collaborations and establish new ones.

The goal is to achieve results of foundational and practical impact. The expected outcome is a novel formal approach to develop and maintain modern applications by focusing on dynamic adaptation, property enforcing and component interaction. Its adoption will drastically improve the quality of SW on which our daily lives rely. IoT scenarios will demonstrate this.