Skip to main content

Modular Specification of Hybrid Systems in Charon

  • Conference paper
  • First Online:

Part of the Lecture Notes in Computer Science book series (LNCS,volume 1790)

Abstract

We propose 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 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.

Keywords

  • Hybrid System
  • Atomic Agent
  • Hybrid Automaton
  • Algebraic Constraint
  • Hierarchical Mode

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This is a preview of subscription content, access via your institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • DOI: 10.1007/3-540-46430-1_5
  • Chapter length: 14 pages
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
eBook
USD   99.00
Price excludes VAT (USA)
  • ISBN: 978-3-540-46430-3
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
Softcover Book
USD   129.00
Price excludes VAT (USA)

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

    MATH  CrossRef  MathSciNet  Google Scholar 

  2. R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, 2000. To appear.

    Google Scholar 

  3. R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee. Charon: a language for modular specification of hybrid systems. Technical Report MS-CIS-2000-01, University of Pennsylvania, 2000.

    Google Scholar 

  4. R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In CONCUR’ 97: Eighth International Conference on Concurrency Theory, LNCS 1243, pages 74–88. Springer-Verlag, 1997.

    Google Scholar 

  5. R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.

    CrossRef  Google Scholar 

  6. G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997.

    Google Scholar 

  7. D.P. Bertsekas and J. N. Tsitsiklis. Parallel and Distributed Computation: Numerical Methods. Athena Scientific, 1997.

    Google Scholar 

  8. A. Deshpande, A. Göllu, and L. Semenzato. The shift programming language and run-time systems for dynamic networks of hybrid automata. Technical Report UCB-ITS-PRR-97-7, University of California at Berkeley, 1997.

    Google Scholar 

  9. R. Grosu, T. Stauner, and M. Broy. A modular visual model for hybrid systems. In Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT’98), LNCS 1486, pages 75–91. Springer-Verlag, 1998.

    CrossRef  Google Scholar 

  10. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.

    MATH  CrossRef  MathSciNet  Google Scholar 

  11. T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th IEEE Real-Time Systems Symposium, pages 56–65, 1995.

    Google Scholar 

  12. N. Lynch, R. Segala, F. Vaandrager, and H. Weinberg. Hybrid I/O automata. In Hybrid Systems III: Verification and Control, LNCS 1066, pages 496–510, 1996.

    Google Scholar 

  13. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Real-Time: Theory in Practice, REX Workshop, LNCS 600, pages 447–484. Springer-Verlag, 1991.

    CrossRef  Google Scholar 

  14. W. Press, S. Teukolsky, W. Vetterling, and B. Flannery. Numerical Recipes in FORTRAN. Cambridge University Press, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I. (2000). Modular Specification of Hybrid Systems in Charon. In: Lynch, N., Krogh, B.H. (eds) Hybrid Systems: Computation and Control. HSCC 2000. Lecture Notes in Computer Science, vol 1790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46430-1_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-46430-1_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67259-3

  • Online ISBN: 978-3-540-46430-3

  • eBook Packages: Springer Book Archive

We’re sorry, something doesn't seem to be working properly.

Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.