Predictive Formal Analysis of Resilience in Cyber-Physical Systems

Abstract

The behavioral analysis of cyber-physical systems in safety-critical scenarios is a challenging task. In this paper, the endogenous and exogenous aspects of resilience are of cornerstone importance in system design and verification. Endogenous resilience is the inherent ability of the system to detect and process internal faults and malicious attacks. Exogenous resilience is the permanent capability of the system to maintain a safe operation within its ambient environment. In this paper, we present a predictive dual-sided contract-based formal methodology to address both aspects of resilience on top of a distributed object-oriented component-based software model. It is illustrated by a case study of urban drone rescue systems. We exploit the formalism of timed automat a and the toolbox UPPAAL to predict by abstraction and analyze (simulate and verify) endogenous resilience. Instead of presenting the final models of the case study, we reflect our experience with UPPAAL in generic patterns of system design and contract specification, reusable in other contexts with adaptations. The analysis of exogenous resilience is specific to the considered drone rescue system. It consists of synthesizing by iterative model-checking safe flight paths for the drones within a 3D virtual model of urban surroundings true to modern cities.