The Timer Cascade: Functional Modelling and Real Time Calculi

  • Raymond Boute
  • Andreas Schäfer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


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 Terms

Automata cascade connection Duration Calculus functional description Funmath hybrid systems real time systems systems modelling timers 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    Alur, R., Henzinger, T.A., Sontag, E.D. (eds.): HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)Google Scholar
  3. 3.
    Bartle, R.G.: The Elements of Real Analysis. Wiley, New York (1964)Google Scholar
  4. 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. 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. 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. 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. 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. 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
  10. 10.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. IPL 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Dijkstra, E.W.: Under the spell of Leibniz’s dream. In: EWD1298 (April 2000)Google Scholar
  12. 12.
    Dijkstra, R.M.: Computation calculus: Bridging a formalization gap. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 151–174. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Gries, D.: The need for education in useful formal logic. IEEE Computer 29(4), 29–30 (1996)Google Scholar
  14. 14.
    Habrias, H., Faucou, S.: Linking Paradigms, Semi-formal and Formal Notations. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 166–184. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Hansen, M.R., Chaochen, Z.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  16. 16.
    Krilavičius, T.: Bestiarium of Hybrid Systems (draft March 2005),
  17. 17.
    Lee, E.A., Varaiya, P.: Structure and Interpretation of Signals and Systems. Addison-Wesley, Reading (2003)Google Scholar
  18. 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
  19. 19.
    Pugh, W.: Counting Solutions to Presburger Formulas: How and Why. ACM SIGPLAN Notices 29(6), 121–122 (1994)CrossRefGoogle Scholar
  20. 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
  21. 21.
    Schäfer, A.: A Calculus for Shapes in Time and Space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  22. 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
  23. 23.
    Vaandrager, F.W., van Schuppen, J.H. (eds.): HSCC 1999. LNCS, vol. 1569. Springer, Heidelberg (1999)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Raymond Boute
    • 1
  • Andreas Schäfer
    • 2
  1. 1.INTECUniversiteit GentBelgium
  2. 2.Department für InformatikUniversität OldenburgGermany

Personalised recommendations