Forrit í náttúrunni: Óvissa, aðlögunarhæfni og sannprófun - verkefni lokið
Fréttatilkynning verkefnisstjóra
Cyber-Physical Systems (CPSs) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. For instance, the dynamic
physical environmental processes can only be approximated in order to become computationally tractable; some agents may appear, disappear, or become temporarily unavailable, thus causing faults or conflicts; sensors may introduce measurement errors; etc.
This means that the behaviour of the agents in a CPS is subject to uncertainty and perturbations. On top of that, there is a class of security threats which is unique to CPSs, namely cyber-physical attacks: for instance, an attacker can induce a series of perturbations in the sensed data in order to entail unexpected, hazardous, behaviour of the system. It is therefore fundamental to verify whether a CPS is robust against perturbations, i.e., whether the system is able to function correctly even in the presence of perturbations.
The main objective of this project was to provide the means to perform this kind of verification.
To this end, we started from the definition of a general framework for modelling CPSs in the
presence of uncertainties, the evolution sequence model, that allows us to consider all possible
systems trajectories at once. Then, we have proposed two different temporal logics, the Robustness Temporal Logic (RobTL) and the Distribution Temporal Logic (DisTL), allowing us to various kinds of robustness requirements on evolution sequences. We have then made our theoretical framework usable in practice by developing the Software Tool for Analysis of Robustness in the unKnown environment (STARK), a Java tool for the specification, analysis and
verification of robustness properties of CPSs that is based on the evolution sequence model from for the representation of systems behaviour, and on RobTL and DisTL for the specification of properties.
All our results are based on a new, fresh, point of view on the problem of studying the effects of
uncertainties on the behaviour of systems. For this reason, our achievements have always stimulated interesting discussions with the community whenever we presented them at conferences, workshops and meetings. Hence, we hope to have inspired other researchers to study our approach and techniques and to apply them to their field, or to solve some problem they are studying. Indeed, we expect STARK to have a major impact on the community, as it can be used to study various kinds of systems, and has also potential applications that go beyond the analysis and verification of CPSs. Nonetheless, this project had a clear impact on the career of the principal investigator, as she was not only able to gain new competences and skills, but also a position as an assistant professor at one of the most renowned universities in Europe.
Information on how the results will be applied:
The entire framework that we developed can be used for the analysis and verification of CPSs, and in general of any system that is subject to uncertainty, from security to bioinformatics.
Moreover, given the uniqueness of its features, and the expressive power of the model and logics on which it is built, our STARK tool can become a game changer in various areas of research. For
instance, we are now planning to use it for the creation of digital twins and the analysis of the
behaviour of AI systems.
A list of the project's outputs:
The list of all the publications, and submitted papers that resulted from the project is, and will
remain, available on the project's web site at https://sites.google.com/view/projectultron/publications.
Overall, the project produced one journal papers, three conference papers, and one book chapters.
Four journal papers resulting from the project are under review. Moreover one article is currently in preparation. All publications are accessible in open access form from the project's web site, as well as from the proposer personal webpage
https://sites.google.com/view/valentinacastiglioni/home/publications
Besides publications, one of the principal outcomes of this project is the Software Tool for Analysis of Robustness in the unKnown environment (STARK), that is available in open access on Github, at
https://github.com/quasylab/jspear/tree/working.
Heiti verkefnis: Forrit í náttúrunni: Óvissa, aðlögunarhæfni og sannprófun/Programs in
the wild: Uncertainties, adaptability and verification
Verkefnisstjóri: Valentina Castiglioni, Háskólanum í Reykjavík
Tegund styrks: Nýdoktorsstyrkur
Styrktímabil: 2022-2023
Fjárhæð styrks kr. 22.933.000
Tilvísunarnúmer Rannís: 228376
