| Abstract: |
By integrating components for sensing, communicating, computing and actuating, Cyber-Physical Systems (CPSs) enable software applications to monitor and control events in the physical world.
It is widely anticipated that CPSs will become pervasive in personal and industrial applications. As deployed CPSs will impact safety of humans and infrastructure, certifying their correctness is
imperative. For an important class of systems, correctness requires guaranteed timing properties. For instance, in an automatic stability program of an automobile, the worst-case end- to-end
delay between sensing and actuating could be upper-bounded. Analysis of such hard real-time guarantees in CPSs is inherently challenging, because the timing models exhibit variability due to
multiple reasons. Firstly, as CPSs are distributed and heterogeneous, events do not arrive periodically. Secondly, on modern processors, resource availability can be non-uniform due to physical
effects such as overheating or low energy supply. Thirdly, timing models can be uncertain either due to incorrect calibration or simultaneous analysis of multiple designs. Finally, due to complex
components in such CPSs, such as caches, rare and transient phenomena can result in deviation from nominal timing models. In three parts of the thesis, we present three templates of solutions to
compute hard real-time guarantees in the presence of the said variability. - Variability in arrival patterns of events can be absorbed by a run-time manager which monitors and adapts to incoming
events. We illustrate this by compositionally building demand bound servers and cool-shapers from efficient constituent units. - Variability in timing models can be bounded with analysis of sound
abstractions which compactly represent the timing-critical traces of the system. We illustrate this with the analysis of temperature- controlled speed-scaling and the analysis of multiple designs
within an Satisfiability Modulo Theory (SMT) solver. - Variability due to rare and transient phenomena can be exported through richer guarantees to verify cross-layer objectives such as stability
of a plant in a networked control system. We illustrate this by proposing and computing settling-time and overshoot metrics. |
