by Davide Basile, Maurice ter Beek, Giovanna Broccia and Alessio Ferrari (ISTI-CNR)
Researchers from the Formal Methods and Tools (FMT) lab of ISTI-CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN).
T-LADIES (Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems) [L1] 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 they provide inadequate support for development and maintenance, automatic property verification and enforcement, and bug detection.
T-LADIES proposes to use dynamic language adaptation to improve the development and maintenance process in combination with advanced type systems to verify and enforce the properties of software systems. The aim is to increase productivity and software quality, while reducing development costs and time-to-market.
T-LADIES focuses on the Internet of Things (IoT), which is characterised by several interconnected "things", typically in Systems of Systems, which have heterogeneous capabilities and behaviour, and whose spatial distribution is a relevant parameter. These characteristics pose several key challenges:
- IoT applications are programmed in general-purpose, domain-agnostic languages, which hinders their maintenance, modification, and evolution. Since IoT is pervasive, it is desirable that domain experts – without advanced programming skills – can easily (re)program, maintain, and modify IoT applications.
- “Things” are assumed to interact according to predefined schemes, whereas context and application changes call for supporting configurations that are unknown when "things" are conceived. Such flexibility requires richer ways to specify "things" capable of improving the approaches typically offered by general-purpose languages.
- IoT applications are based on the interaction of "things" that dynamically vary in number and kind, which poses issues of correctness, dynamic evolution, and adaptation. The notion of interaction should thus be enriched to support variability, dynamic monitoring, property enforcing, and orchestration of the "things" in the general context of Systems of Systems.
- IoT applications and systems have to meet high-quality standards, like absence of undesired situations (e.g., deadlocks, orphan messages, etc.), support for non-functional requirements (e.g., performance, energy sustainability, etc.), and resilience to varying or reconfigurable execution contexts. The complexity of IoT applications and Systems of Systems makes it hard to meet and preserve such standards without automated tools.
T-LADIES addresses these challenges through an approach to software development that mixes language adaptation, interaction mechanisms, and advanced type systems. In T-LADIES, language adaptation will make it possible to vary how the language behaves in different contexts and, consequently, to modify application behaviour accordingly, with no impact on the source code. Interaction protocols are intended to provide extra functionality to the mechanisms that are natively available in the context in which the application runs. Advanced type systems enable the behavioural specification of entities, the enforcing and verification of system properties, and the early detection of bugs.
The overall goal is to achieve results of both 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. In particular, based on experience in studying compositionality in terms of configurability and adaptability at runtime, and on formal methods and tools for guaranteeing safe communication in Systems of Systems modeled as (contract or team) automata [R1], FMT will introduce variability in multi-party synchronisation type specifications and interaction protocols, as well as criteria to preserve communication properties (e.g., receptiveness, responsiveness, agreement, etc.) by composition, akin to the correctness-by-construction paradigm.
Adoption of the aforementioned novel formal approach will drastically improve the quality of software on which our daily lives rely. Case studies from the IoT domain will drive the research and demonstrate the effectiveness of the approach. In particular, building on experience in developing and analysing IoT and railway systems in EU projects [R2], and exploiting background in requirements elicitation from domain experts, FMT will empirically investigate the effectiveness of the proposed techniques and methodologies on application scenarios related to the smart maintenance and monitoring of the Italian socio-ecosystem with its inherent variability. This will be carried out by means of case-study research, with structured and rigorous protocols [R3], in order to ensure empirical evidence and provide the involved practitioners with a clear view of the potential of the approach, while revealing practical challenges (e.g., tool usability, technical skills required, etc.) that can help to fine-tune the project's output. Furthermore, FMT will perform evaluations of human factors (e.g., usability, comprehensibility, etc.) in IoT software design and implementation.
T-LADIES will run until May 2025 and is coordinated by Walter Cazzola from the University of Milan. Other partners are the University of Catania, the University of Genoa, the University of Modena and Reggio Emilia, and ISTI-CNR.
Link:
[L1] https://t-ladies.di.unimi.it/
References:
[1] D. Basile, M.H. ter Beek, “Contract Automata Library”, Sci. Comput. Program, 2022. http://doi.org/10.1016/j.scico.2022.102841
[2] A. Ferrari, F. Mazzanti, D. Basile, M.H. ter Beek, “Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signaling System Design”, IEEE Trans. Software Eng., 2021. https://doi.org/10.1109/TSE.2021.3124677
[3] M.H. ter Beek, A. Ferrari, “Empirical Formal Methods: Guidelines for Performing Empirical Studies on Formal Methods”, Software, 2022. https://doi.org/10.3390/software1040017
Please contact:
Maurice ter Beek or Alessio Ferrari
ISTI-CNR, Italy
