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 thernphysical environment that they monitor and actuate on. CPS have to adapt online to the changingrnnature of the physical environment; this may require the online modification of their systemrnmodel, but any change should preserve correct operation. Correctness by construction relies onrnusing formal tools, which suffer from a considerable computational overhead. As the currentrnsystem model of a CPS may adapt to the environment, the new system model must be verifiedrnbefore its execution to ensure that the properties are preserved. However, CPS development hasrnmainly concentrated on the design-time aspects, existing only few contributions that addressrntheir online adaptation. We research on the pros and cons of formal tools to support dynamicrnchanges at runtime. We formalize the semantics of the adaptation logic of an autonomic managerrn(OLIVE) that performs online verification for a specific application, a dynamic virtualizedrnserver system.We explore the use of formal tools based on CLTLoc to express functional and nonfunctionalrnproperties of the system.We provide empirical results showing the temporal costs ofrnour approach.