Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Hybrid Systems: Computation and Control

HSCC 2001: Hybrid Systems: Computation and Control pp 33–48Cite as

Compositional Refinement for Hierarchical Hybrid Systems

  • Conference paper
  • First Online:

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

Abstract

In this paper, we develop a theory of modular design and refinement of hierarchical hybrid systems. In particular, we present compositional trace-based semantics for the language Charon that allows 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. We develop an observational trace semantics for agents as well as for modes, and define a notion of refinement for both, based on trace inclusion. We show this semantics to be compositional with respect to the constructs in the language.

This research was supported in part by NSF CCR-9988409, ARO DAAG55-98-1-0466, DARPA ITO MOBIES F33615-00-C-1707, DARPA ITO MARS program, grant no. 130-1303-4-534328-xxxx-2000-0000, and ONR N00014-97-1-0505 (MURI).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

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.

    Article  MATH  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, pages 390–402, 2000.

    Google Scholar 

  3. R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee. Modular specifications of hybrid systems in Charon. In Hybrid Systems: Computation and Control, Third International Workshop, volume LNCS 1790, pages 6–19, 2000.

    Chapter  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. G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997.

    Google Scholar 

  6. J. Davis, M. Goel, C. Hylands, B. Kienhuis, E.A. Lee, J. Liu, X. Liu, L. Muliadi, S. Neuendorfier, J. Reekie, N. Smyth, J. Tsay, and Y. Xiong. Overview of the Ptolemy project. Technical Report UCB/ERL M99/37, University of California at Berkeley, 1999.

    Google Scholar 

  7. A. Deshpande, A. Göllu, and P. Varaiya. SHIFT: a formalism and a programming language for dynamic networks of hybrid automata. In Hybrid Systems V, LNCS 1567. Springer, 1996.

    Google Scholar 

  8. R. Grosu, T. Stauner and M. Broy. A Modular Visual Model for Hybrid Systems. In FTRTFT’98: Formal Techniques in Real Time and Fault Tolerant Systems, LNCS 1486. Springer-Verlag, 1998.

    Chapter  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  10. T.A. Henzinger. Masaccio: a formal model for embedded components. In TCS 00: Theoretical Computer Science, LNCS 1872, pages 549–563. Springer, 2000.

    Google Scholar 

  11. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    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.

    Chapter  Google Scholar 

  14. R. Milner. A Calculus of Communicating Systems. LNCS 92. Springer-Verlag, 1980.

    MATH  Google Scholar 

Download references

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radu Grosu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Insup Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Oleg Sokolsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Ingegneria Elettrica, Universitá dell’Aquila, Poggio di Roio, 67040, L’Aquila, Italy

    Maria Domenica Di Benedetto

  2. University of California at Berkeley, Berkeley, CA, 94720

    Alberto Sangiovanni-Vincentelli

  3. PARADES, Via San Pantaleo, 66, 00186, Roma, Italy

    Alberto Sangiovanni-Vincentelli

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Grosu, R., Lee, I., Sokolsky, O. (2001). Compositional Refinement for Hierarchical Hybrid Systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2001. Lecture Notes in Computer Science, vol 2034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45351-2_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-45351-2_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41866-5

  • Online ISBN: 978-3-540-45351-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation