|
CHARON: Hierarchical Specification and Analysis of Hybrid Systems
Rajeev Alur
Abstract
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.
|
