TY - JOUR
T1 - A refinement-based process algebra for timed automata
AU - Cattani, Stefano
AU - Kwiatkowska, Marta
PY - 2005/8/1
Y1 - 2005/8/1
N2 - We propose a real-time extension to the process algebra CSR 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.
AB - We propose a real-time extension to the process algebra CSR 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.
UR - http://www.scopus.com/inward/record.url?scp=23844489391&partnerID=8YFLogxK
U2 - 10.1007/s00165-005-0064-y
DO - 10.1007/s00165-005-0064-y
M3 - Article
SN - 1433-299X
SN - 1433-299X
SN - 1433-299X
SN - 1433-299X
VL - 17
SP - 138
EP - 159
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 2
ER -