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.
The project is structured in the following 6 work-packages.
WP1 - Models and Languages will apply graph-based models to smart system scenarios in order to fully exploit the naturalness of such models. It will extend the concurrency theory of graph manipulation formalisms and identify suitable fragments of existing logics, interpreted over graphs, balancing expressiveness and usability.
[WP leader: Gadducci, UNIPI]
WP2 - Systems Analysis will develop tools and techniques for supporting design-time analysis of smart systems at different levels of abstraction in order to predict their emerging behaviour and measure the ability of the systems to adapt autonomously to highly dynamic operational environments.
[WP leader: Loreti, UNICAM]
WP3 - from Models to Code will define a new programming framework resulting from the integration of the classic Event-Condition-Action paradigm with attribute-based and aggregate programming. The framework will support runtime monitoring.
[WP leader: Miculan, UNIUD]
WP4 - Runtime Monitoring will characterize the fragments of the studied logics that can be verified and enforced at runtime, and develop monitor synthesis procedures, suitable instrumentation mechanisms and prototype runtime monitoring tools.
[WP leader: Aceto, GSSI]
WP5 - Application and Validation will demonstrate the feasibility and impact of the various techniques, methodologies and tools developed during the project by applying them to three challenging smart-system scenarios of direct importance to some project partners and related stakeholders.
[WP leader: ter Beek, ISTI-CNR]
WP6 - Dissemination will disseminate the results of the project internally, within the scientific community and, via the three cases studies, to a variety of stakeholders.
[WP leader: De Nicola, IMT]