It is easy to write and verify real-time specifications with existing languages and methods; one just represents time as an ordinary variable and expresses timing requirements with special timer variables. The resulting specifications can be verified with an ordinary model checker. This basic idea and some less obvious details are explained, and results are presented for two examples.


Model Checker Reachable State Time Translation State Predicate Ordinary Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16(5), 1543–1571 (1994)CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
  3. 3.
    Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 199–214. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Graf, S., Loiseaux, C.: Property preserving abstractions under parallel composition. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 644–657. Springer, Heidelberg (1993)Google Scholar
  5. 5.
    Henzinger, T.A., Kupferman, O.: From quantity to quality. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 48–62. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  6. 6.
    Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)Google Scholar
  7. 7.
    Lamport, L.: Proving possibility properties. Theoretical Computer Science 206(1–2), 341–352 (1998)CrossRefMathSciNetzbMATHGoogle Scholar
  8. 8.
    Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2003); A link to an electronic copy can be found at, Google Scholar
  9. 9.
    Lamport, L.: Real time is really simple. Technical Report MSR-TR-2005-30, Microsoft Research (March 2005)Google Scholar
  10. 10.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal of Software Tools for Technology Transfer 1(1/2), 134–152 (1997)CrossRefzbMATHGoogle Scholar
  11. 11.
    McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)zbMATHGoogle Scholar
  12. 12.
    Perlman, R.: An algorithm for distributed computation of a spanningtree in an extended LAN. In: Proceedings of the Ninth Symposium on Data Communications. SIGCOMM, pp. 44–53. ACM Press, New York (1985)CrossRefGoogle Scholar
  13. 13.
    Schneider, F.B., Bloom, B., Marzullo, K.: Putting time into proof outlines. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 618–639. Springer, Heidelberg (1992)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Leslie Lamport
    • 1
  1. 1.Microsoft Research 

Personalised recommendations