The goal of the project is the development and the experimentation of a novel methodology for the specification, implementation and validation of trustworthy smart systems based on formal methods. We envisage system development in three steps by first providing and analysing system models to find design errors, then moving from models to executable code by translation into domain-specific programming languages and, finally, monitoring runtime execution to detect anomalous behaviours and to support systems in taking context-dependent decisions autonomously.
The project’s scientific and technological impact will produce results from which Italian industry, Italian economy and, in the long term, Italian society may benefit. Scientifically, the research will yield new, fundamental insights on the general properties of large scale, physically located, smart systems, leading to an end-to-end, principled approach to their design, implementation and deployment. The developed software tools and the work on the case studies will show the effectiveness of our proposed approach in three practical scenarios at different application scales, will reduce the gap between theory and practice, and will demonstrate the use of our techniques to Italian industry and society.