The Open UniversitySkip to content
 

Compositional Verification of Self-Adaptive Cyber-Physical Systems

Borda, Aimee; Pasquale, Liliana; Koutavas, Vasileios and Nuseibeh, Bashar (2018). Compositional Verification of Self-Adaptive Cyber-Physical Systems. In: 13th ACM/IEEE International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), 28-29 May 2018, Gothenburg, Sweden.

Full text available as:
[img]
Preview
PDF (Accepted Manuscript) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (842kB) | Preview
DOI (Digital Object Identifier) Link: https://doi.org/10.1145/3194133.3194146
Google Scholar: Look up in Google Scholar

Abstract

Cyber-Physical Systems (CPSs) must often self-adapt to respond to changes in their operating environment. However, using formal verification techniques to provide assurances that critical requirements are satisfied can be computationally intractable due to the large state space of self-adaptive CPSs. In this paper we propose a novel language, Adaptive CSP, to model self-adaptive CPSs modularly and provide a technique to support compositional verification of such systems. Our technique allows system designers to identify (a subset of) the CPS components that can affect satisfaction of given requirements, and define adaptation procedures of these components to preserve the requirements in the face of changes to the system’s operating environment. System designers can then use Adaptive CSP to represent the system including potential selfadaptation procedures. The requirements can then be verified only against relevant components, independently from the rest of the system, thus enabling computationally tractable verification. Our
technique enables the use of existing formal verification technology to check requirement satisfaction. We illustrate this through the use of FDR, a refinement checking tool. To achieve this, we provide an adequate translation from a subset of Adaptive CSP to the language of FDR. Our technique allows system designers to identify alternative adaptation procedures, potentially affecting different sets of CPS components, for each requirement, and compare them based on correctness and optimality. We demonstrate the feasibility of our approach using a substantive example of a smart art gallery. Our results show that our technique reduces the computational complexity of verifying self-adaptive CPSs and can support the design of adaptation procedures.

Item Type: Conference or Workshop Item
Copyright Holders: 2018 ACM
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Item ID: 54307
Depositing User: Danielle Lilly
Date Deposited: 23 Apr 2018 10:48
Last Modified: 07 Dec 2018 11:47
URI: http://oro.open.ac.uk/id/eprint/54307
Share this page:

Metrics

Altmetrics from Altmetric

Citations from Dimensions

Download history for this item

These details should be considered as only a guide to the number of downloads performed manually. Algorithmic methods have been applied in an attempt to remove automated downloads from the displayed statistics but no guarantee can be made as to the accuracy of the figures.

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU