Modular specification of hybrid systems in Charon

DOI10.1007/3-540-46430-1_5MaRDI QIDQ4953375zbMATH OpenFDO

Authors Radu Grosu, Yerang Hur, Vijay Kumar, Insup Lee, Rajeev Alur

Publication date 8 September 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46430-1_5

zbMATH Keywords

Charoncomplex agentsdecentralized simulationhierarchical descriptioninteracting hybrid systemsinvariantsmodular simulationmodular specificationsystem architecture

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Software, source code, etc. for problems pertaining to systems and control theory (93-04) Hierarchical systems (93A13) Decentralized systems (93A14) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Review text

A new language, called Charon, is proposed for modular specification of interacting hybrid systems. For a hierarchical description of the system architecture, Charon supports building complex agents via the operations of instantiation, hiding, and parallel composition. For a hierarchical description of the behaviour of atomic components, it 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 behaviour. The continuous behaviour 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. The authors illustrate this aspect by presenting a scheme for modular simulation in which each mode can be compiled solely based on the locally declared information to execute its discrete and continuous updates, and furthermore, submodes can integrate at a finer time scale than the enclosing modes. For the entire collection see [Zbl 0934.00029].

Recommendations

• scientific article; zbMATH DE number 2080748
• Compositional modeling and refinement for hierarchical hybrid systems
• scientific article; zbMATH DE number 1794359
• Hybrid Systems: Computation and Control
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Cited in

(17)

• An algebra of hybrid systems
• Modeling and simulation of cardiac tissue using hybrid I/O automata
• Compositional modeling and refinement for hierarchical hybrid systems
• Algorithmic analysis of polygonal hybrid systems. I: Reachability
• Monotonic hybrid systems
• Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point
• Spatial networks of hybrid I/O automata for modeling excitable tissue
• A Formal Framework for User Centric Control of Probabilistic Multi-agent Cyber-Physical Systems
• Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
• Bio-PEPA with Events
• scientific article; zbMATH DE number 2080748 (Why is no real title available?)
• scientific article; zbMATH DE number 1794359 (Why is no real title available?)
• Synthesizing SystemC Code from Delay Hybrid CSP
• A Hybrid Denotational Semantics for Hybrid Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Hybrid Systems: Computation and Control
• Modular and visual specification of hybrid systems: An introduction to HyCharts

Describes a project that uses

Uses Software

• Charon

This page was built for publication: Modular specification of hybrid systems in Charon

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4953375)