Charon

CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. For hierarchical description of the system architecture, CHARON provides the operations of instantiation, hiding, and parallel composition on agents, which can be used to build a complex agent from other agents. The discrete and continuous behaviors of an agent are described using modes. For hierarchical description of the behavior of an agent, CHARON supports the operations of instantiation and nesting of modes. Furthermore, 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 also reflected in the semantics so that it can be exploited during analysis.

VO Integration: No

Active: Yes

Available Benchmarks: N/A

Website: https://rtg.cis.upenn.edu/mobies/charon/

Download: Instructions can be found here.

Documentation: A draft manual can be found here. A separate document on the visual editor is here.

Contact: Here is a list of people associated with the tool.

Excerpt and graphics from: https://rtg.cis.upenn.edu/mobies/charon/

Each agent can be represented as a parallel composition of sub-agents. Each atomic agent consists of one top-level mode.

Each agent consists of one top-level mode or behavior. However, modes can in turn consist of submodes. A mode describes flow of control inside an agent.