Cyber-physical systems (CPS) are large scale systems highly integrated with the physical environment. Given the changing nature of physical environments, CPS must be able to adapt on-line to new situations while preserving their correct operation. Correctness by construction relies on using formal tools, which suffer from a considerable computational overhead especially if executed on-line. As the current system model of a CPS may change to adapt to the environment, the new system model has to be verified at run-time prior to its execution to ensure that the system properties are preserved. CPS development has mainly concentrated on the design-time aspects, existing only few contributions that support on-line adaptation. We undertake a practical exercise to research on the pros and cons of formal tools to support dynamic changes at run-time. We formalize the semantics of the adaptation logic of an autonomic manager (OLIVE) that performs on-line verification for a specific application, i.e., a dynamic virtualized server system. We explore the realization of the autonomic manager using formal tools based on CLTLoc to express functional and non-functional properties of the managed system. The on-line verification manager services requests from mobile clients that might require a change inboth the running software components and server services. To establish if the adaptation preserves the temporal constraints provided in the specification, i.e., to decide whether a new client request can be serviced in the modified system, the on-line verification manager employs CLTLoc satisfiability checking. In this scenario, we then provide empirical results showing thetemporal costs of our approach.
The Cost of Formal Verification in Adaptive CPS. An Example of a Virtualized Server Node
Bersani M. M.;
2016-01-01
Abstract
Cyber-physical systems (CPS) are large scale systems highly integrated with the physical environment. Given the changing nature of physical environments, CPS must be able to adapt on-line to new situations while preserving their correct operation. Correctness by construction relies on using formal tools, which suffer from a considerable computational overhead especially if executed on-line. As the current system model of a CPS may change to adapt to the environment, the new system model has to be verified at run-time prior to its execution to ensure that the system properties are preserved. CPS development has mainly concentrated on the design-time aspects, existing only few contributions that support on-line adaptation. We undertake a practical exercise to research on the pros and cons of formal tools to support dynamic changes at run-time. We formalize the semantics of the adaptation logic of an autonomic manager (OLIVE) that performs on-line verification for a specific application, i.e., a dynamic virtualized server system. We explore the realization of the autonomic manager using formal tools based on CLTLoc to express functional and non-functional properties of the managed system. The on-line verification manager services requests from mobile clients that might require a change inboth the running software components and server services. To establish if the adaptation preserves the temporal constraints provided in the specification, i.e., to decide whether a new client request can be serviced in the modified system, the on-line verification manager employs CLTLoc satisfiability checking. In this scenario, we then provide empirical results showing thetemporal costs of our approach.File | Dimensione | Formato | |
---|---|---|---|
2016_HASE_MGV_MMB_camera_ready_v04.pdf
accesso aperto
:
Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione
390.12 kB
Formato
Adobe PDF
|
390.12 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.