Notes:
The original publication is available at link.springer.com.
|
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 advantage of our proposal
is that it is possible to automatically verify refinement relations between
processes. We demonstrate how this can be achieved and under which
conditions.
|