Compositonal modelling and verification of self-adaptive cyber-physical systems

Abstract

Cyber-Physical Systems (CPSs) must often self-adapt to respond to changes in their operating environment. However, providing assurances of critical requirements through formal verification techniques can be computationally intractable due to the large state space of self-adaptive CPSs. In this thesis we propose a methodology to support assurances of such systems, which employs a novel modelling language, Adaptive CSP, enabling compositional reasoning for tractable verification. The process language extends Communicating Sequential Processes (CSP) with constructs to reduce the effort required to model and compositionally verify the adaptation options and events of self-adaptive CPSs.

Our methodology allows system designers to identify (a subset of) the CPS components that can affect satisfaction of each given requirement. An adaptation procedure for these components can then be created to preserve the requirement in the face of changes to the system?s operating environment. Although manual, the task of identifying components relevant to a requirement can be guided by topological relationships, such as containment and connectivity between system components. Adaptive CSP can then be used to model the system including potential self-adaptation procedures. We propose a modular structure for adaptation procedures which, together with topology-guided adaptation, allows system designers to compare alternative adaptation procedures, potentially involving different sets of CPS components.

We show that with this approach, when different requirements involve disjoint sets of components, verification of each requirement can be performed against only its relevant components, in isolation from the rest of the system and other adaptation procedures. When components are relevant for multiple requirements, we develop a theory of compositionality to identify cases where interference between adaptation procedures is not possible. We prove that in such cases requirement verification can still be performed in isolation from other adaptation procedures and the rest of the system. In the other cases, the system designer must additionally verify that requirement satisfaction is preserved when components with corresponding adaptation procedures from interdependent requirements are composed.

Our methodology has the benefit of leveraging existing formal verification tools to check requirement satisfaction. We illustrate this through the use of FDR - an existing refinement checker for CSP, taking advantage of its advanced model minimisation and refinement checking functionality. The soundness of using FDR for verification relies on an adequate translation from a subset of Adaptive CSP to the language of FDR. We also alleviate the onus of modelling and verifying components in our framework further by providing a concrete syntax to Adaptive-CSP, where we augment the process language with convenient idioms and macros from functional languages, together with a tool which translates Adaptive-CSP code to FDR.

We demonstrate the feasibility of our methodology using a substantive motivating example of a smart art gallery. We further evaluate it with a case study of a smart stadium. Our results show that our methodology reduces the computational complexity of verifying self-adaptive CPSs and can effectively support the design of adaptation procedures in such systems.