Write a Blog >>
SEAMS 2018
Mon 28 - Tue 29 May 2018 Gothenburg, Sweden
co-located with * ICSE 2018 *
Mon 28 May 2018 11:00 - 11:25 at E1 room - Qualities & Verification Chair(s): Radu Calinescu

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 self-adaptation 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 ofAdaptive 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.

Mon 28 May
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Qualities & VerificationSEAMS 2018 at E1 room
Chair(s): Radu CalinescuUniversity of York, UK
11:00
25m
Compositional Verification of Self-Adaptive Cyber-Physical SystemsLong Paper
SEAMS 2018
Aimee BordaTrinity College Dublin, Liliana PasqualeUniversity College Dublin & Lero, Ireland, Vasileios Koutavas, Bashar NuseibehThe Open University (UK) & Lero (Ireland)
Pre-print
11:25
15m
DeSiRE: Further Understanding Nuances of Degrees of Satisfaction of Non-functional Requirements Trade-offShort Paper
SEAMS 2018
Ross Edwards, Nelly BencomoAston University
11:40
15m
RE-STORM: Mapping the Decision-Making Problem and Non-Functional Requirements Trade-off to Partially Observable Markov Decision ProcessesShort Paper
SEAMS 2018
Luis Garcia PaucarAston University, Nelly BencomoAston University
11:55
15m
Towards Integrating Undependable Self-Adaptive Systems in Safety-Critical EnvironmentsShort Paper
SEAMS 2018
Gereon WeissFraunhofer ESK, Philipp SchleissFraunhofer ESK, Daniel SchneiderFraunhofer IESE, Mario TrappFraunhofer IESE
12:10
15m
K8-Scalar: a workbench to compare autoscalers for container-orchestrated database clustersArtifact
SEAMS 2018
Wito DelnatKatholieke Universiteit Leuven, Eddy TruyenKatholieke Universiteit Leuven, Ansar RafiqueKatholieke Universiteit Leuven, Dimitri Van LanduytKatholieke Universiteit Leuven, Wouter JoosenKatholieke Universiteit Leuven