학술논문

Runtime Equilibrium Verification for Resilient Cyber-Physical Systems
Document Type
Conference
Source
2021 IEEE International Conference on Autonomic Computing and Self-Organizing Systems (ACSOS) ACSOS Autonomic Computing and Self-Organizing Systems (ACSOS), 2021 IEEE International Conference on. :71-80 Sep, 2021
Subject
Communication, Networking and Broadcast Technologies
Computing and Processing
Robotics and Control Systems
Runtime
Uncertainty
Conferences
Cyber-physical systems
Markov processes
Bayes methods
Robots
runtime verification
resilience
viability zone
equilibrium
uncertainty
Language
Abstract
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.