Modeling the Simplex Architecture using Charon

Charon is a language for the hierarchical and modular speciication of interacting hybrid systems and is based on the notions of agent and mode. It has well-deened formal semantics, and can be used to specify precisely hybrid systems that exhibit continuous behaviors within modes and discrete jumps between modes. The goal of the Simplex Architecture is to support the reliable upgrade of control software on the y, and thus, it requires delicate and complex mode switching between diierent controllers. Due to complexity, it is a quite challenging task to show the correctness of control software built using the Sim-plex Architecture. As a rst step toward addressing the challenge, this paper shows that how the Simplex Architecture can be speciied in Charon using the well-known inverted pendulum system.