Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Hybrid Systems: Computation and Control

HSCC 1999: Hybrid Systems: Computation and Control pp 223–237Cite as

Refinement and Continuous Behaviour

  • Conference paper
  • First Online:

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

Abstract

Refinement Calculus is a formal framework for the development of provably correct software. It is used by Action Systems, a predicate transformer based framework for constructing distributed and reactive systems. Recently, Action Systems were extended with a new action called the differential action. It allows the modelling of continuous behaviour, such that Action Systems may model hybrid systems. In this paper we investigate how the differential action fits into the refinement framework. As the main result we develop simple laws for proving a refinement step involving continuous behaviour within the Refinement Calculus.

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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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.J.R. Back. Refinement calculus, part II: Parallel and reactive programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. 1989, volume 430 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

    Google Scholar 

  2. R.J.R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 131–142, 1983.

    Google Scholar 

  3. R.J.R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming,12, pp. 17–30, 1991.

    Google Scholar 

  4. R.J.R. Back and J. von Wright. Trace Refinement of Action Systems. In J. Parrow, editor, CONCUR94, LNCS 666, Springer-Verlag, 1994.

    Google Scholar 

  5. R.J.R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, Springer-Verlag,1998.

    Google Scholar 

  6. M.S. Branicky. Studies in Hybrid Systems: Modeling, Analysis, and Control. PhD Thesis. Massachusetts Institute of Technology, EECS Dept, 1995.

    Google Scholar 

  7. M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In J-R. Abrial, E. Borger, H. Langmaack (eds.) Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, Springer-Verlag, 1996.

    Chapter  Google Scholar 

  8. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.

    Google Scholar 

  9. T.A. Henzinger, Z. Manna, and A. Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel (eds.) Hybrid Systems, LNCS 736, Springer-Verlag, 1993.

    Chapter  Google Scholar 

  10. T.A. Henzinger and P.-H. Ho. HyTech: The Cornell hybrid technology tool. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, LNCS 999, pp. 265–293, Springer-Verlag, 1995.

    Chapter  Google Scholar 

  11. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations Part II: Timing-based systems. Information and Computation, 128(1):1–25, July 1996.

    Article  MathSciNet  Google Scholar 

  12. Brendan P. Mahony and Ian J. Hayes. A Case-Study in Timed Refinement: A Mine Pump. IEEE Transactions on Software Engineering, vol. 18, no. 9, September 1992.

    Google Scholar 

  13. M.H.A. Newman. Elements of the Topology of Plane Sets of Points. Cambridge University Press, 1961 (First edition 1939).

    Google Scholar 

  14. M. Rönkkö and A.P. Ravn. Action Systems with Continuous Behaviour. To appear in the Proceedings of Hybrid Systems V-Fifth International Hybrid Systems Workshop, LNCS, Springer-Verlag, 1998.

    Google Scholar 

  15. M. Rönkkö and A.P. Ravn. Switches and Jumps in Hybrid Action Systems. Proceedings of the Estonian Academy of Sciences. Engineering, June 1998, 4,2, pp. 106–118.

    Google Scholar 

  16. M. Rönkkö and K. Sere. Refinement and Continuous Behaviour. No. 198 (updated version), Technical Reports, Turku Centre for Computer Science,Åbo Akademi University, Finland, September 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Turku Centre for Computer Science, Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14A, FIN, 20520, Turku, Finland

    Mauno Rönkkö

  2. Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14A, FIN-20520, Turku, Finland

    Kaisa Sere

Authors
  1. Mauno Rönkkö
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kaisa Sere
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500, GL, Nijmegen, The Netherlands

    Frits W. Vaandrager

  2. CWI, P.O. Box 94079, 1090, GB, Amsterdam, The Netherlands

    Jan H. van Schuppen

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rönkkö, M., Sere, K. (1999). Refinement and Continuous Behaviour. In: Vaandrager, F.W., van Schuppen, J.H. (eds) Hybrid Systems: Computation and Control. HSCC 1999. Lecture Notes in Computer Science, vol 1569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48983-5_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-48983-5_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65734-7

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation