The Timer Cascade: Functional Modelling and Real Time Calculi
- 354 Downloads
Case studies can significantly contribute towards improving the understanding of formalisms and thereby to their applicability in practice. One such case, namely a cascade of the familiar 24-hour timers (in suitably generalized form) provides interesting gedanken experiments and illustrations for presenting, illustrating and comparing various formalisms for modelling real-time behaviour of systems.
The timer cascade is first modelled in a general-purpose functional formalism (Funmath) and various properties are derived, including an interesting algebraic monoid structure of timer programs. Then it is described and analyzed in duration calculus, thereby highlighting, similarities and differences in the approach to modelling and reasoning, and also the link between the formalisms.
Future work consists in using this case as a running example for exploring the same issues for other formalisms intended for real time and hybrid systems. The underlying idea is that other authors join this effort and contribute towards extending it, finally arriving at a broad comparative survey of such formalisms.
Index TermsAutomata cascade connection Duration Calculus functional description Funmath hybrid systems real time systems systems modelling timers
Unable to display preview. Download preview PDF.
- 1.Almstrum, V.L.: Investigating Student Difficulties With Mathematical Logic. In: Neville Dean, C., Hinchey, M.G. (eds.) Teaching and Learning Formal Methods, pp. 131–160. Academic Press, London (1996)Google Scholar
- 2.Alur, R., Henzinger, T.A., Sontag, E.D. (eds.): HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)Google Scholar
- 3.Bartle, R.G.: The Elements of Real Analysis. Wiley, New York (1964)Google Scholar
- 4.Boute, R.T.: Funmath illustrated: A Declarative Formalism and Application Examples. Declarative Systems Series No. 1, Computing Science Institute, University of Nijmegen (1993)Google Scholar
- 5.Boute, R.: Functional Mathematics: a Unifying Declarative and Calculational Approach to Systems, Circuits and Programs — Part I: Basic Mathematics, Course text, Ghent University (2002)Google Scholar
- 6.Boute, R.T.: Concrete Generic Functionals: Principles, Design and Applications. In: Gibbons, J., Jeuring, J. (eds.) Generic Programming, pp. 89–119. Kluwer, Dordrecht (2003)Google Scholar
- 7.Boute, R.: Functional declarative language design and predicate calculus: a practical approach. To appear in ACM Trans. Prog. Lang. and Syst.Google Scholar
- 8.Boute, R.: Calculational semantics: deriving programming theories from equations by functional predicate calculus. To appear in ACM Trans. Prog. Lang. and Syst.Google Scholar
- 9.Buck, J., Ha, S., Lee, E.A., Messerschmitt, D.G.: Ptolemy: a framework for simulating and prototyping heterogeneous systems. International Journal of Computer Simulation, spec. issue on Simulation Software Development (January 1994)Google Scholar
- 11.Dijkstra, E.W.: Under the spell of Leibniz’s dream. In: EWD1298 (April 2000)Google Scholar
- 13.Gries, D.: The need for education in useful formal logic. IEEE Computer 29(4), 29–30 (1996)Google Scholar
- 16.Krilavičius, T.: Bestiarium of Hybrid Systems (draft March 2005), http://wwwhome.cs.utwente.nl/~krilaviciust/publications/bestiarium.pdf
- 17.Lee, E.A., Varaiya, P.: Structure and Interpretation of Signals and Systems. Addison-Wesley, Reading (2003)Google Scholar
- 18.Pandya, P.K.: Specifying and deciding qauntified discrete-time duration calculus formulae using dcvalid. Technical report, Tata Institute of Fundamental Research (2000)Google Scholar
- 20.Schäfer, A.: Combining Real-Time Model-Checking and Fault Tree Analysis. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003), http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/as03.pdf Google Scholar
- 22.Smith, G.: Specifying Mode Requiremens of Embedded Systems. In: Oudshoorn, M., et al. (eds.) ACSC 2002, January–February 2002, pp. 251–257 (2002), Also http://www.itee.uq.edu.au/~smith/papers/acsc2002.pdf