Paper Info
Title
Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs.
Abstract
Cyber-physical systems (CPS) are highly dynamic and large scale systems integrated with the physical environment that they monitor and actuate on. CPS have to adapt online to the changing nature of the physical environment; this may require the online modification of their system model, but any change should preserve correct operation. Correctness by construction relies on using formal tools, which suffer from a considerable computational overhead. As the current system model of a CPS may adapt to the environment, the new system model must be verified before its execution to ensure that the properties are preserved. However, CPS development has mainly concentrated on the design-time aspects, existing only few contributions that address their online adaptation. We research on the pros and cons of formal tools to support dynamic changes at runtime. We formalize the semantics of the adaptation logic of an autonomic manager (OLIVE) that performs online verification for a specific application, a dynamic virtualized server system. We explore the use of formal tools based on CLTLoc to express functional and nonfunctional properties of the system. We provide empirical results showing the temporal costs of our approach.
Year
DOI
Venue
2018
10.1002/smr.1880
JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS
Keywords
Field
DocType
Cyber-physical systems,linear temporal logic,real-time,resource management,verification,virtualization
Resource management,Virtualization,Overhead (computing),Software engineering,Computer science,Correctness,Linear temporal logic,Cyber-physical system,System model,Semantics,Distributed computing
Journal
Volume
Issue
ISSN
30.0
SP3.0
2047-7473
Citations 
PageRank 
References 
4
0.41
6
Authors
2
Name
Order
Citations
PageRank
Marcello M. Bersani112816.06
Marisol García-Valls254040.75