Advertisement

Abstract

We present a process algebra suitable to the modelling of timed concurrent systems and to their efficient verification through model checking. The algebra is provided with two consistent semantics: a structural operational semantics (as usual for process algebras) and a denotational semantics in terms of Petri nets in which time is introduced through counters of explicit clock ticks. This way of modelling time has been called causal time so the process algebra is itself called the Causal Time Calculus (CTC). It was shown in a separate paper that the causal time approach allowed for efficient verification but suffered from a sensitivity to the constants to which counts of ticks are compared. We show in this paper how this weakness can be removed.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2). Elsevier (1994)Google Scholar
  2. 2.
    Best, E., Devillers, R., Hall, J.: The Petri Box Calculus: a new causal algebra with multilabel communication. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, Springer, Heidelberg (1992)Google Scholar
  3. 3.
    Bui Thanh, C., Klaudel, H., Pommereau, F.: Petri nets with causal time for system verification. In: MTCS 2002. Electronic Notes in Theoretical Computer Sciences, vol. 68.5, Elsevier, Amsterdam (2002)Google Scholar
  4. 4.
    Bui Thanh, C., Klaudel, H., Pommereau, F.: Box Calculus with Coloured Buffers. LACL Technical report (2002), Available at http://www.univ-paris12.fr/lacl
  5. 5.
    Corradini, F., D’Ortenzio, D., Inverardi, P.: On the relationship among four timed process algebras. Fundamenta Informaticae 34. IOS Press (1999)Google Scholar
  6. 6.
    D’Argenio, P.R.: Algebras and automata for real-time systems. PhD. Thesis, Department of Computer Science, University of Twente (1999)Google Scholar
  7. 7.
    Durchholz, R.: Causality, time, and deadlines. Data & Knowledge Engineering 6. North-Holland (1991)Google Scholar
  8. 8.
    Esparza, J.: Model checking using net unfoldings. Science of Computer Programming 23. Elsevier (1994)Google Scholar
  9. 9.
    Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 582. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Khomenko, V., Koutny, M.: Branching processes of high-level Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 458–472. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Koutny, M.: A compositional model of time Petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 303. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journalon Software Tools and Technology Transfer 1(1-2). Springer (1997)Google Scholar
  13. 13.
    Mäkelä, M.: MARIA: modular reachability analyser for algebraic system nets (1999), Online manual http://www.tcs.hut.fi/maria
  14. 14.
    Marroquín Alonzo, O., de Frutos Escrig, D.: Extending the Petri Box Calculus with time. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, p. 303. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Merlin, P.M., Farber, D.J.: Recoverability of communication protocols—implications of a theoretical study. IEEE Transaction on Communication 24. IEEE Society (1976)Google Scholar
  16. 16.
    Milner, R.: Communication and concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  17. 17.
    Plotkin, G.D.: A Structural approach to Operational Semantics. Technical Report FN-19, Computer Science Department, University of Aarhus (1981)Google Scholar
  18. 18.
    Pommereau, F.: Causal Time Calculus. LACL Technical report (2002), Available at http://www.univ-paris12.fr/lacl
  19. 19.
    Ramchandani, C.: Analysis of asynchronous concurrent systems using Petri nets. PhD. Thesis, project MAC, MAC-TR 120. MIT (1974)Google Scholar
  20. 20.
    Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1/2). Springer (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Franck Pommereau
    • 1
  1. 1.LACL, Université Paris 12CréteilFrance

Personalised recommendations