A calculus for hybrid sampled data systems
This paper addresses the problem of formally describing hybrid sampled data systems. Using the techniques proposed in Duration Calculus, we first develop a formal calculus, called Accumulation Calculus, for specifying real valued step functions of time. The key idea is that such functions are described using their integrals in bounded closed intervals. The semantics of Accumulation Calculus formulae as well as a relatively complete axiom system are presented.
Sampled data are a particular type of step functions which change at regular periods only. Suitable axioms are introduced to capture this. Special formulae and modalities are introduced to describe such data. Some proof rules are proposed for these modalities and shown to be sound. Resulting system is called a calculus for hybrid sampled data systems. Well established representations of sampled data systems from control theory such as difference equations can be directly translated into such formulae. At the same time the calculus allows reasoning about asynchronous events and their effect on sampled data. A detailed case study of a heating system is given to illustrate the applicability of the calculus to hybrid sampled data systems.
KeywordsDifference Equation Hybrid System Boolean Function Heat System Predicate Symbol
Unable to display preview. Download preview PDF.
- 1.H.Barringer, R.Kuiper and A.Pnueli, A really abstract concurrent model and its temporal logic, Proceedings 13th ACM Symposium on the Principles of Programming Languages, pp.173–183, 1986.Google Scholar
- 2.W.J.Bencze and G.F.Franklin, A separation principle for hybrid control system design, to appear in the Proceedings of the 1994 IEEE/IFAC Symposium on Computer-Aided Control System Design, to be held March 7–9, 1994 in Tuscon, Arizona.Google Scholar
- 3.R.C.Dorf, Modern Control Systems, Fifth Edition, Addison-Wesley Publishing Company, Inc., 1989.Google Scholar
- 4.G.F.Franklin and J.D.Powell and M.L.Workman, Digital Control of Dynamic Systems, Second Edition, Addison-Wesley Publishing Company, 1990.Google Scholar
- 5.R.L.Grossman, A.Nerode, H.Rischel, and A.P.Ravn(Eds.), Hybrid Systems, LNCS 736, Springer-Verlag Berlin Heidelberg 1993.Google Scholar
- 6.M.R.Hansen and Zhou Chaochen, Semantics and completeness of duration calculus, Proceedings of Real-Time: Theory in Practice, REX Workshop, Mook, the Netherlands, LNCS 600, pp.209–225, 1992.Google Scholar
- 7.J.Hooman, A compositional approach to the design of hybrid systems, in R.L.Grossman, A.Nerode, H.Rischel, and A.P.Ravn(Eds.), Hybrid Systems, LNCS 736, pp.121–148, Springer-Verlag Berlin Heidelberg 1993.Google Scholar
- 8.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
- 9.O.Maler, Z.Manna and A.Pnueli, From timed to hybrid systems, in J.W. de Bakker, C.Huizing, W.-P. de Roever and G.Rozenberg (Eds.) Real-Time: Theory in Practice, REX Workshop, pp.447–484, LNCS600,1992Google Scholar
- 10.Z.Manna and A.Pnueli, Models for reactivity, Acta Informatica 30, pp.609–678, Springer-Verlag 1993.Google Scholar
- 11.B. Moszkowski, A temporal logic for multilevel reasoning about hardware, IEEE Computer, 18(2):10–19, 1985.Google Scholar
- 12.Yu Xinyao, Wang Ji, Zhou Chaochen and Paritosh K. Pandya, Formal design of hybrid systems, UNU/IIST Report No.19, 1994.Google Scholar
- 13.Zhou Chaochen, C.A.R.Hoare and A.P.Ravn, A calculus of durations, Information Processing Letters, 40(5):269–276, 1992.Google Scholar
- 14.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