Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs

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.