Skip to main content

Formal design of hybrid systems

  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1994, ProCoS 1994)

Abstract

A hybrid system is a system containing both of time-evolving components and event-driven components. A formal approach is explored in this paper, based on Extended Duration Calculus (EDC), for the development of hybrid systems. A typical example of hybrid system from modern control theory, a two-level adaptive control system, is used for illustrating our approach. Its high level consists of an event-driven supervisor which reacts to the change of plant structure, and its time-evolving low level consists of adaptive controllers and other components. Firstly performance specifications and system specification of the case are formulated in EDC; then they are refined stepwise into specifications of the supervisor and the low level components. Our approach emphasizes the interface between the two kinds of components in the hybrid system.

This research is supported by DeTfoRS Project funded by The National Hi-Tech R & D Programme of China and UNU/IIST.

On leave from Department of Automatic Control, Beijing University of Aeronautics and Astronautics, Beijing 100083, China.

On leave from Department of Computer Science, Changsha Institute of Technology, Changsha 4100T3, China.

On leave from Computer Science Group, Tata Institute of Fundamental Research, Homi Bhabha Road, Bombay 400005, India.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis and T.A. Henzinger, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, in R.L.Grossman, A. Nerode, H. Rischel, and A.P. Ravn(Eds.), Hybrid Systems, LNCS 736, pp.209–229, Springer-Verlag Berlin Heidelberg 1993.

    Google Scholar 

  2. K.J. åström and B. Wittenmark, Adaptive Control, Addison-Wesley Publishing Company, 1989.

    Google Scholar 

  3. W.J. Bencze and G.F. Franklin, A separation principle for hybrid control system design, in the proceedings of the 1994 IEEE/IFAC Symposium on Computer-Aided Control System Design, March 7–9, 1994 in Tuscon, Arizona.

    Google Scholar 

  4. Chen Zongji and P.A. Cook, Robustness of model reference adaptive control systems with unmodeled dynamics, I. J. Control, 39 (1984), 201–204.

    Google Scholar 

  5. M. Engel, M. Kubica, J. Madey, D.L. Parnas, A.P. Ravn and A.J. van Schnowen, A Formal Approach to Computer Systems Requirements Documentation, in R.L. Grossman, A. Nerode, H. Rischel, and A.P. Ravn(Eds.), Hybrid Systems, LNCS 736, pp.452–474, Springer-Verlag Berlin Heidelberg 1993.

    Google Scholar 

  6. G.F. Franklin, J.D. Powell and A. Emami-Naeini, Feedback Control of Dynamic Systems, Addison-Wesley, Reading, Mass, 1986.

    Google Scholar 

  7. Ho Yu-chi and Xi-Ren Cao, Perturbation Analysis of Discrete Event Dynamic System, Kluwer Academic Publishers, Boston, Dordreecht, London, 1991.

    Google Scholar 

  8. M.R. Hansen, Zhou Chaochen, J. Staunstrup: A Real-Time Duration Semantics for Circuits, Proc. of the Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton, March 1992

    Google Scholar 

  9. He Jifeng, From CSP to Hybrid Systems, in A Classical Mind, Essays in Honour of C. A. R. Hoare, A. W. Roscoe (ed.), Prentice Hall International, 1994.

    Google Scholar 

  10. L. Lamport, Hybrid systems in TLA + in R.L.Grossman, A.Nerode, H.Rischel, and A.P.Ravn(Eds.), Hybrid Systems, LNCS 736, pp.77–102, Springer-Verlag Berlin Heidelberg 1993.

    Google Scholar 

  11. Z. Manna and A. Pnueli, Verifying Hybrid Systems, in R.L. Grossman, A. Nerode, H. Rischel, and A.P. Ravn(Eds.), Hybrid Systems, LNCS 736, pp.4–35, Springer-Verlag Berlin Heidelberg 1993.

    Google Scholar 

  12. A.P. Ravn, H. Rischel: Requirements Capture for Embedded Real-Time Systems, Proc. IMACS-MCTS'91 Symp. Modelling and Control of Technological Systems, Vol 2, pp. 147–152, Villeneuve d'Ascq, France, 1991.

    Google Scholar 

  13. J.U. SkakkebÆk, A.P. Ravn, H. Rischel, Zhou Chaochen: Specification of Embedded Real-Time Systems, Proc. 4th Euromicro Workshop on Real-Time Systems, IEEE Press, pp 116–121, June 1992

    Google Scholar 

  14. Wang Ji, Yu Xinyao and Zhou Chaochen, Refinement of Digital Dynamic Systems, UNU/IIST Technical Report No. 20, 1994.

    Google Scholar 

  15. Zhou Chaochen, C. A. R. Hoare, A. P. Ravn, A calculus of durations, Information Processing Letters 40(5), 1991: 269–276.

    Google Scholar 

  16. Zhou Chaochen, A. P. Ravn, M. R. Hansen, An extended duration calculus for hybrid real-time systems, in R.L. Grossman, A. Nerode, H. Rischel, and A.P. Ravn(Eds.), Hybrid Systems, LNCS 736, pp.36–59, Springer-Verlag Berlin Heidelberg 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Hans Langmaack Willem-Paul de Roever Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Xinyao, Y., Ji, W., Chaochen, Z., Pandya, P.K. (1994). Formal design of hybrid systems. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_193

Download citation

  • DOI: https://doi.org/10.1007/3-540-58468-4_193

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58468-1

  • Online ISBN: 978-3-540-48984-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics