CHARON: Hierarchical Specification and Analysis of Hybrid Systems

Rajeev Alur


We describe a language, called CHARON, for modular specification of interacting hybrid systems. For hierarchical description of the system architecture, CHARON supports building complex agents via the operations of instantiation, hiding, and parallel composition. For hierarchical description of the behavior of atomic components, CHARON supports building complex modes via the operations of instantiation, scoping, and encapsulation. Features such as weak preemption, history retention, and externally defined Java functions, facilitate the description of complex discrete behavior. Continuous behavior can be specified using differential as well as algebraic constraints, and invariants restricting the flow spaces, all of which can be declared at various levels of the hierarchy. The modular structure of the language is not merely syntactic, but can be exploited during analysis. We illustrate this aspect by presenting (1) a scheme for modular simulation in which submodes can integrate at a finer time scale than the enclosing modes, (2) a compositional trace semantics for modes with refinement calculus, and (3) heuristics for symbolic model checking for the discrete subset that exploit the hierarchical structure. The application domains for CHARON include autonomous robots and biomolecular networks.

©2002-2018 U.C. Regents