Opacity Verification and Fault Diagnosis in the Framework of Switching Output Automata

Security and reliability in cyber-physical systems depend not only on which operational mode the system occupies, but also on how long it remains there. In practice, external observers see piecewise-constant output signals (power consumption levels, alarm indicators, aggregate measurements) together with their durations, rather than internal state transitions or continuous trajectories. Classical discrete-event models capture event sequences but lack native timing semantics, while dense-time formalisms such as timed automata face undecidability or prohibitive complexity for verification tasks involving both timing constraints and partial observability. This dissertation introduces the Switching Output Automaton (SOA) framework to address this gap. SOA models what observers see in practice: output symbols and their durations. The key innovation is a minimum dwell time constraint that requires any two consecutive events to be separated by at least a fixed positive duration. This constraint reflects physical reality and enables decidable verification by bounding the rate of observable changes. SOA combines continuous-time semantics with a set-valued output function that creates observational ambiguity independent of timing, allowing multiple states to share output symbols. We apply this framework to two timing-aware security and reliability problems. First, for opacity verification, we establish decidable procedures for both current-state opacity (where secrets are discrete states) and timed opacity (where secrets are global-state-duration triples specifying which combinations of discrete state, output, and dwell time must remain confidential). For timed opacity, verification proceeds by constructing a secret-dependent evolution automaton that applies fine-grained time discretization only to vulnerable global states, then building an observer automaton through subset construction, and finally reducing opacity to reachability analysis. This approach achieves decidability without the severe restrictions required for timed automata, keeping complexity within the observer-based determinization profile familiar from untimed discrete-event systems. Second, for timed fault diagnosis, we extend SOA to a Switching Output Automaton with Faults (SOAF) that models faults enabled only during specific dwell-time windows in fault-prone states. This captures degradation phenomena where failures emerge from sustained exposure to stress conditions rather than instantaneous events. Diagnosis proceeds through a four-stage construction: logical state discretization preserving fault-window boundaries, evolution automaton with faults construction tracking nominal and fault transitions, fault recognizer synthesis with observation mappings, and subset determinization yielding an online diagnoser that classifies observation sequences as normal, faulty, or uncertain with sound and complete detection guarantees. Three case studies validate the framework across safety-critical domains. A smart water supply system verifies current-state opacity under aggregate power monitoring, demonstrating that critical pump-valve configurations remain hidden from adversaries observing power consumption. A patient monitoring system verifies timed opacity for healthcare privacy, ensuring prolonged critical-condition patterns remain indistinguishable from benign fluctuations through network observations. A battery management system applies timed fault diagnosis to thermal runaway detection, illustrating how health-dependent fault window parameterization reduces detection delay. To support reproducibility, we provide an open-source implementation of the verification framework.