University of Limerick Institutional Repository

Compositional verification of self-adaptive cyber-physical systems

DSpace Repository

Show simple item record

dc.contributor.author Borda, Aimee
dc.contributor.author Pasquale, Liliana
dc.contributor.author Koutavas, Vasileios
dc.contributor.author Nuseibeh, Bashar
dc.date.accessioned 2018-12-18T16:07:28Z
dc.date.available 2018-12-18T16:07:28Z
dc.date.issued 2018
dc.identifier.uri http://hdl.handle.net/10344/7425
dc.description peer-reviewed en_US
dc.description.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. en_US
dc.language.iso eng en_US
dc.publisher Assocation for Computing Machinery en_US
dc.relation ASAP en_US
dc.relation.ispartofseries ;pp. 1-11
dc.relation.uri http://dx.doi.org/10.1145/3194133.3194146
dc.rights © ACM, 2018. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SEAMS '18 Proceedings of the 13th International Conference on Software Engineering for Adaptive and Self-Managing Systems,pp.1-11, en_US
dc.subject software and its engineering en_US
dc.subject system modeling languages en_US
dc.subject formal software verification en_US
dc.title Compositional verification of self-adaptive cyber-physical systems en_US
dc.type info:eu-repo/semantics/conferenceObject en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.identifier.doi 10.1145/3194133.3194146
dc.contributor.sponsor SFI en_US
dc.contributor.sponsor ERC en_US
dc.relation.projectid 13/RC/2094 en_US
dc.relation.projectid 15/SIRG/3501 en_US
dc.relation.projectid 291652 en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


Browse

My Account

Statistics