Adaptive cyber-physical systems rely on the composition and coordinated interaction of different decision-making procedures. Cyber components capabilities and semantics are usually captured by operational models (such as automata) and modal logics. Physical components and their controllers are instead formalized via dynamical systems of equations, primarily structured by the laws of Physics.
The heterogeneity of these mathematical formalisms makes it difficult to formalize and reason about cross-cutting properties emerging from the interaction of the discrete-event logic used to manage cyber components and the differential equations used to control the physical parts of the system. Such properties involve both functional requirements of the system — what it is supposed to do — and non-functional ones — how reliable, secure, performant, or expensive its operations can be.
To complete the picture, intrinsic randomness, partial observability, and limited measurability of both the physical environment and the internal state of off-the-shelf software components require means to represent uncertainty and its propagation across all the levels of decision making, with additional challenges in terms of expressiveness and complexity.
The goal of this PhD project is to investigate design and verification techniques at the interface between cyber and physical elements. In particular, the identification of what information they should share and how the different mathematical abstractions capturing each element’s semantics can be reconciled to allow engineering more effective, runtime-efficient, and secure adaptation strategies.