Aleksandrov, AndreiAndreiAleksandrovVöllinger, KimKimVöllinger2024-12-092024-12-092025https://publica.fraunhofer.de/handle/publica/47980710.1007/978-3-031-77019-7_20Switched systems (i.e. systems switching between a finite set of continuous systems) are an important subclass of hybrid systems, expressive enough for a wide range of systems. This paper introduces the first formalization of switched systems in the proof assistant Coq - a step towards building verified controllers in Coq. We define switched systems and the trajectories they induce while prioritizing verification. Moreover, we offer a specialized formalization for the efficient modeling of periodic controllers. Finally, we illustrate the formalization by modeling and verifying an air filter.enFormal languages and automata theoryLogicDesign and analysis of algorithmsProbabilistic programmingSemantics and reasoningModels of computationconference paper