Paper Info
Title
The Cost of Formal Verification in Adaptive CPS. An Example of a Virtualized Server Node
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 in both 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 the temporal costs of our approach.
Year
DOI
Venue
2016
10.1109/HASE.2016.46
2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE)
Keywords
Field
DocType
Cyber-physical systems,virtualization,resource management,real-time,linear temporal logic,verification
Software engineering,Computer science,Correctness,Server,Node (networking),Real-time computing,Linear temporal logic,Cyber-physical system,Component-based software engineering,System model,Reliability engineering,Formal verification
Conference
ISSN
Citations 
PageRank 
1530-2059
7
0.55
References 
Authors
15
2
Name
Order
Citations
PageRank
Marcello M. Bersani112816.06
Marisol García-Valls254040.75