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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
R.J.R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming,12, pp. 17–30, 1991.
R.J.R. Back and J. von Wright. Trace Refinement of Action Systems. In J. Parrow, editor, CONCUR94, LNCS 666, Springer-Verlag, 1994.
R.J.R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, Springer-Verlag,1998.
M.S. Branicky. Studies in Hybrid Systems: Modeling, Analysis, and Control. PhD Thesis. Massachusetts Institute of Technology, EECS Dept, 1995.
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.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
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.
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.
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.
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.
M.H.A. Newman. Elements of the Topology of Plane Sets of Points. Cambridge University Press, 1961 (First edition 1939).
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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