Runtime Equilibrium Verification for Resilient Cyber-Physical Systems
Cyber-Physical Systems are the basis of more and more activities in our modern society. Therefore, providing comprehensive, ideally provable, evidence that they continuously exhibit acceptable behavior even in case of unexpected events represents a major challenge that is not completely addressed by existing verification approaches.
To this end, in this paper we exploit the notion of equilibrium, i.e., the ability of the system to maintain an acceptable behavior within its multidimensional viability zone and we propose RUNE (RUNtime Equilibrium verification), an approach able to verify at runtime if the system satisfies the equilibrium condition. RUNE includes (i) a system specification that takes into account the uncertainties related to partial knowledge and possible changes by adopting parametric Markov decision processes; (ii) the computation of the equilibrium condition to define the boundaries of the viability zone; and (iii) a runtime equilibrium verification method that leverages on Bayesian inference to reduce the uncertainty under the required level and quantitatively reason about the ability of the system to remain inside the boundaries of the viability zone. We demonstrate the benefits of the proposed approach on a running example from the robotics domain.
Thu 30 SepDisplayed time zone: Eastern Time (US & Canada) change
11:45 - 12:40 | Languages, formal methods, and assurances for Autonomic and Self-Organizing SystemsMain Track at AUDITORIUM 2 Chair(s): Roberto Casadei University of Bologna, Italy | ||
11:45 25mPaper | Runtime Equilibrium Verification for Resilient Cyber-Physical Systems Main Track Matteo Camilli Free University of Bozen-Bolzano, Raffaela Mirandola Politecnico di Milano, Patrizia Scandurra University of Bergamo, Italy | ||
12:10 15mShort-paper | A Programming Language for Sound Self-Adaptive Systems Main Track Media Attached | ||
12:25 15mVision and Emerging Results | Towards Mapping Control Theory and Software Engineering Properties using Specification Patterns Main Track Ricardo Caldas Chalmers, Razan Ghzouli Chalmers University of Technology & University of Gothenburg, Alessandro Vittorio Papadopoulos Mälardalen University, Patrizio Pelliccione Gran Sasso Science Institute (GSSI) and Chalmers | University of Gothenburg, Danny Weyns KU Leuven, Thorsten Berger Chalmers | University of Gothenburg Pre-print |