CHARON is a language for the hierarchical and modular
specification of interacting hybrid systems and is based on the
notions of agent and mode. It has well-defined 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 fly, and thus, it requires delicate and complex mode
switching between different controllers. Due to complexity, it is a
quite challenging task to show the correctness of control software
built using the simplex architecture. As a first step toward
addressing the challenge, this paper shows that how the simplex
architecture can be specified in CHARON using the well-known
inverted pendulum system.
