ACSOS 2021
Mon 27 September - Fri 1 October 2021 Washington, DC, United States

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 Sep

Displayed 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
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
A Programming Language for Sound Self-Adaptive Systems
Main Track
Barry Porter Lancaster University, Roberto Vito Rodrigues Filho Federal University of Goiás
Media Attached
Vision 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