Skip to main content

Advertisement

Springer Nature Link
Log in

Modular and Visual Specification of Hybrid Systems: An Introduction to HyCharts

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Visual description techniques are particularly important for the design of hybrid systems, because specifications of such systems usually have to be discussed between engineers from a number of different disciplines. Modularity is vital for hybrid systems not only because it allows to handle large system, but also because it permits to think in terms of components, which is familiar to engineers.

Based on two different interpretations for hierarchic graphs and on a clear hybrid computation model, we develop HyCharts. HyCharts consist of two modular visual formalisms, one for the specification of the architecture and one for the specification of the behavior of hybrid systems. The operators on hierarchic graphs enable us to give a surprisingly simple denotational semantics for many concepts known from statechart-like formalisms. Due to a very general composition operator, HyCharts can easily be composed with description techniques from other engineering disciplines. Such heterogeneous system specifications seem to be particularly appropriate for hybrid systems because of their interdisciplinary character.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (France)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Google Scholar 

  2. R. Alur and D.L. Dill, “A theory of timed automata,” Theoretical Computer Science, Vol. 126, pp. 183-235, 1994.

    Google Scholar 

  3. R. Alur and T.A. Henzinger, “Modularity for timed and hybrid systems,” in CONCUR 97: Concurrency Theory, LNCS, Vol. 1243, Springer-Verlag, Berlin, 1997.

  4. J.F. Broenink, “Modelling, simulation and analysis with 20-Sim,” Journal A, the special issue on CACSD, Vol. 97, No. 3, pp. 22-25, 1997.

    Google Scholar 

  5. M. Broy, “Refinement of time,” in ARTS'97, LNCS, Vol. 1231, Springer-Verlag, Berlin, 1997.

    Google Scholar 

  6. Z. Chaochen, A.P. Ravn, and M.R. Hansen, “An extended duration calculus for hybrid real-time systems,” in Hybrid Systems, LNCS, Vol. 736, Springer-Verlag, Berlin, 1993.

    Google Scholar 

  7. R. Engelking, General Topology, Vol. of Sigma Series in Pure Mathematics, Heldermann Verlag, Berlin, 1989.

    Google Scholar 

  8. S. Engell and I. Hoffmann, “Modular hierarchical models of hybrid systems,” in Proc. of the 35th IEEE Conference on Decision and Control (CDC), Kobe, 1996, pp. 142-143.

  9. G. Fábián, D.A. van Beek, and J.E. Rooda, “Integration of the discrete and the continuous behaviour in the hybrid chi simulator,” in 1998 European Simulation Multiconference, Manchester, 1998, pp. 252-257.

  10. R. Grosu, M. Broy, B. Selic, and Gh. Stefănescu, “Towards a calculus for UML-RT specifications,” in 7th OOPSLA Workshop on Behavioral Semantics of OO Business and System Specifications, Technical Report TUM-I9820, Technische Universität München, 1998.

  11. R. Grosu, M. Broy, B. Selic, and Gh. Stefănescu, “What is behind UML-RT?” in Behavioral Specifications of Businesses and Systems, Kluwer Academic Publishers, Dordrecht, 1999.

    Google Scholar 

  12. R. Grosu and T. Stauner, “Visual description of hybrid systems,” in Workshop On Real Time Programming (WRTP'98), Elsevier Science Ltd., New York, 1998.

    Google Scholar 

  13. R. Grosu, T. Stauner, and M. Broy, “Amodular visual model for hybrid systems,” in Proc. of Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98), LNCS, Vol. 1486, Springer-Verlag, Berlin, 1998.

    Google Scholar 

  14. R. Grosu, Gh. Stefănescu, and M. Broy, “Visual formalisms revisited,” in Proc. Int. Conf. on Application of Concurrency to System Design (CSD), IEEE, 1998.

  15. D. Harel, “Statecharts: A visual formalism for complex systems,” Science of Computer Programming, Vol. 8, 1987.

  16. Y. Kesten and A. Pnueli, “Timed and hybrid statecharts and their textual representation,” in Proc. of Formal Techniques in Real-Time and Fault-Tolerant Systems, 2nd International Symposium, LNCS, Vol. 571, Springer-Verlag, Berlin, 1992.

    Google Scholar 

  17. M. Kloas, V. Friesen, and M. Simons, “Smile-a simulation environment for energy systems,” in Proc. of the 5th International IMACS-Symposium on Systems Analysis and Simulation (SAS'95), Systems Analysis Modelling Simulation, Vol. 18/19, Gordon and Breach Publishers, 1995, pp. 503-506.

    Google Scholar 

  18. L. Lamport, “Hybrid systems in TLA+,” in R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel (Eds.), Hybrid Systems, LNCS, Vol. 736, Springer-Verlag, Berlin, 1993.

    Google Scholar 

  19. N.A. Lynch, R. Segala, F.W. Vaandrager, and H.B. Weinberg, “Hybrid I/O automata,” in Hybrid Systems III, LNCS, Vol. 1066, Springer-Verlag, Berlin, 1996.

    Google Scholar 

  20. P.J. Mosterman, “An overview of hybrid simulation phenomena and their support by simulation packages,” in Hybrid Systems Computation and Control (HSCC'99), LNCS, Vol. 1569, Springer-Verlag, Berlin, 1999.

    Google Scholar 

  21. O. Müller and T. Stauner, “Modelling and verification using linear hybrid automata-a case study,” Mathematical and Computer Modelling of Dynamical Systems, Vol. 6, No. 1, pp. 71-89, 2000.

    Google Scholar 

  22. A. Pnueli, “Development of hybrid systems,” in Proc. of FTRTFT'94, LNCS, Vol. 863, Springer Verlag, Berlin, 1994.

    Google Scholar 

  23. B. Selic, G. Gullekson, and P.T. Ward, Real-Time Object-Oriented Modeling, John Wiley and Sons Ltd., Chichester, 1994.

    Google Scholar 

  24. E.D. Sontag, Mathematical Control Theory, Springer Verlag, Berlin, 1990.

    Google Scholar 

  25. T. Stauner, O. Müller, and M. Fuchs, “Using HyTech to verify an automotive control system,” in Proc. Hybrid and Real-Time Systems (HART'97), LNCS, Vol. 1201, Springer-Verlag, Berlin, 1997.

    Google Scholar 

  26. Gh. Stefănescu, “Algebra of flownomials,” Technical Report TUM-I9437, Technische Universität München, 1994.

  27. The MathWorks Inc. Stateflow. http://www.mathworks.com/products/stateflow/, 1998.

  28. R. Wieting, “Hybrid high-level nets,” in Proceedings of the 1996 Winter Simulation Conference, Coronado, California, USA/Charnes, 1996, pp. 848-855.

  29. K. Wöllhaf, M. Fritz, C. Schulz, and S. Engell, “BaSiP-batch process simulation with dynamically recon-figured process dynamics,” in Proc. of ESCAPE-6, Supplement to Comp. & Chem. Engineering, Vol. 972, No. 20, pp. 1281-1286, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, State University of New York at Stony Brook, Stony Brook, NY, 11794-4400, USA

    Radu Grosu

  2. Institut für Informatik, Technische Universität München, D-80290, München, Germany

    Thomas Stauner

Authors
  1. Radu Grosu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Stauner
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Grosu, R., Stauner, T. Modular and Visual Specification of Hybrid Systems: An Introduction to HyCharts. Formal Methods in System Design 21, 5–38 (2002). https://doi.org/10.1023/A:1016001318739

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1016001318739

Search

Navigation