Oxford logo
[CK03] S. Cattani and M. Kwiatkowska. CSP + Clocks: a process algebra for timed automata. In M. Leuschel and S. Gruner and S. Lo Presti (editors), Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03), pages 50-63. April 2003. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (83 KB)  pdf pdf (264 KB)  bib bib
Abstract. We propose a real-time extension to the process algebra CSP. Inspired by timed automata, a very successful formalism for the specification and verification of real-time systems, we handle real time by means of clocks, i.e. real-valued variables that increase at the same rate as time. This differs from the conventional approach based on timed transitions. We give a discrete trace and failures semantics to our language and define the resulting refinement relations. One of the main advantages of our proposal is that it is possible to automatically verify relations between processes; we will show how this can be done and under which conditions.